Fixed a bug about raising over nominal constants.

When a goal formula G in {L |- G} is proved by backchaining
on some clause F in L or in the program. The clause F should
be raised over all nominal constants in {L |- G} instead of only
those in G.

As an example, the following judgment cannot be proved by Abella
before the fix,

   {of n1 (arr n2 T), of n3 n2 |- of (app n1 n3) T}

where the definition for 'of' is as follows:

   of : tm -> ty -> o.
   of (app M N) T :- of M (arr T1 T), of N T1.

This is because M, N, T1 are raised over n1,n3, but not n2.
As a result, the backchaining produces two subgoals

  {of n1 (arr n2 T), of n3 n2 |- of n1 (arr (T1' n1 n3) T)}
  {of n1 (arr n2 T), of n3 n2 |- of n3 (T1' n1 n3)}

Neither can be proved.

After the bug fix, the backchaining produces the following subgoals

  {of n1 (arr n2 T), of n3 n2 |- of n1 (arr (T1' n1 n2 n3) T)}
  {of n1 (arr n2 T), of n3 n2 |- of n3 (T1' n1 n2 n3)}

which can be proved by instantiating T1' with (x\y\z\ y).