diff -r a8ebcb368a15 -r e5fa8de0e4bd Nominal/nominal_thmdecls.ML
--- a/Nominal/nominal_thmdecls.ML	Thu Jan 06 23:06:45 2011 +0000
+++ b/Nominal/nominal_thmdecls.ML	Fri Jan 07 02:30:00 2011 +0000
@@ -74,7 +74,7 @@
 fun is_eqvt ctxt trm =
   case trm of 
     (c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c
-  | _ => raise TERM ("Term must be a constsnt.", [trm])
+  | _ => false (* raise TERM ("Term must be a constant.", [trm]) *)
 
 
 
@@ -89,13 +89,21 @@
    | Abs (_, _, t) => get_perms t 
    | _ => []
 
-fun put_perm p trm =
-  case trm of 
-     Bound _ => trm
-   | Const _ => trm
-   | t $ u => put_perm p t $ put_perm p u
-   | Abs (x, ty, t) => Abs (x, ty, put_perm p t)
-   | _ => mk_perm p trm
+fun add_perm p trm =
+  let
+    fun aux trm = 
+      case trm of 
+        Bound _ => trm
+      | Const _ => trm
+      | t $ u => aux t $ aux u
+      | Abs (x, ty, t) => Abs (x, ty, aux t)
+      | _ => mk_perm p trm
+  in
+    strip_comb trm
+    ||> map aux
+    |> list_comb
+  end  
+
 
 (* tests whether there is a disagreement between the permutations, 
    and that there is at least one permutation *)
@@ -132,7 +140,7 @@
       then error (msg ^ "(constants do not agree).")
     else if is_bad_list (p :: ps)  
       then error (msg ^ "(permutations do not agree).") 
-    else if not (rhs aconv (put_perm p t))
+    else if not (rhs aconv (add_perm p t))
       then error (msg ^ "(arguments do not agree).")
     else if is_Const t 
       then safe_mk_equiv thm
@@ -175,7 +183,7 @@
       then error (msg ^ "(constants do not agree).")
     else if is_bad_list ps  
       then error (msg ^ "(permutations do not agree).") 
-    else if not (concl aconv (put_perm (the p) prem)) 
+    else if not (concl aconv (add_perm (the p) prem)) 
       then error (msg ^ "(arguments do not agree).")
     else 
       let