--- a/Nominal-General/nominal_thmdecls.ML	Sun Apr 25 08:18:06 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Sun Apr 25 09:13:16 2010 +0200
@@ -45,7 +45,8 @@
 
 fun get_ps trm =
   case trm of 
-     Const (@{const_name permute}, _) $ p $ (Bound _) => raise TERM ("get_ps", [trm])
+     Const (@{const_name permute}, _) $ p $ (Bound _) => 
+       raise TERM ("get_ps called on bound", [trm])
    | Const (@{const_name permute}, _) $ p $ _ => [p]
    | t $ u => get_ps t @ get_ps u
    | Abs (_, _, t) => get_ps t 
@@ -59,7 +60,8 @@
    | Abs (x, ty, t) => Abs (x, ty, put_p p t)
    | _ => mk_perm p trm
 
-(* tests whether the lists of ps all agree, and that there is at least one p *)
+(* tests whether there is a disagreement between the permutations, 
+   and that there is at least one permutation *)
 fun is_bad_list [] = true
   | is_bad_list [_] = false
   | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true
@@ -88,8 +90,7 @@
 
 fun add_raw_thm thm = 
   case prop_of thm of
-    Const ("==", _) $ _ $ _ => 
-      EqvtRawData.map (Item_Net.update (zero_var_indexes thm))
+    Const ("==", _) $ _ $ _ => (EqvtRawData.map o Item_Net.update) thm
   | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) 
 
 val del_raw_thm = EqvtRawData.map o Item_Net.remove;
@@ -98,7 +99,7 @@
 (** transformation of eqvt lemmas **)
 
 
-(* transforms equations into the "p o c = c"-form 
+(* transforms equations into the "p o c == c"-form 
    from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *)
 
 fun eqvt_transform_eq_tac thm = 
@@ -113,18 +114,21 @@
 
 fun eqvt_transform_eq ctxt thm = 
 let
-  val ((p, t), rhs) = apfst dest_perm 
-    (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)))
-    handle TERM _ => error "Eqvt lemma is not of the form p \<bullet> c...  = c..."
+  val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))
+    handle TERM _ => error "Equivariance lemma must be an equality."
+  val (p, t) = dest_perm lhs 
+    handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c...  = c..."
+
   val ps = get_ps rhs handle TERM _ => []  
   val (c, c') = (head_of t, head_of rhs)
+  val msg = "Equivariance lemma is not of the right form "
 in
   if c <> c' 
-    then error "Eqvt lemma is not of the right form (constants do not agree)"
+    then error (msg ^ "(constants do not agree).")
   else if is_bad_list (p::ps)  
-    then error "Eqvt lemma is not of the right form (permutations do not agree)" 
+    then error (msg ^ "(permutations do not agree).") 
   else if not (rhs aconv (put_p p t))
-    then error "Eqvt lemma is not of the right form (arguments do not agree)"
+    then error (msg ^ "(arguments do not agree).")
   else if is_Const t 
     then safe_mk_equiv thm
   else 
@@ -135,14 +139,16 @@
       Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1)
       |> singleton (ProofContext.export ctxt' ctxt)
       |> safe_mk_equiv
+      |> zero_var_indexes
     end
 end
 
-(* transforms equations into the "p o c = c"-form 
+(* transforms equations into the "p o c == c"-form 
    from R x1 ...xn ==> R (p o x1) ... (p o xn) *)
 
-fun eqvt_transform_imp_tac thy p p' thm = 
+fun eqvt_transform_imp_tac ctxt p p' thm = 
 let
+  val thy = ProofContext.theory_of ctxt
   val cp = Thm.cterm_of thy p
   val cp' = Thm.cterm_of thy (mk_minus p')
   val thm' = Drule.cterm_instantiate [(cp, cp')] thm
@@ -154,18 +160,18 @@
 
 fun eqvt_transform_imp ctxt thm =
 let
-  val thy = ProofContext.theory_of ctxt
   val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm))
   val (c, c') = (head_of prem, head_of concl)
   val ps = get_ps concl handle TERM _ => []  
   val p = try hd ps
+  val msg = "Equivariance lemma is not of the right form "
 in
   if c <> c' 
-    then error "Eqvt lemma is not of the right form (constants do not agree)"
+    then error (msg ^ "(constants do not agree).")
   else if is_bad_list ps  
-    then error "Eqvt lemma is not of the right form (permutations do not agree)" 
+    then error (msg ^ "(permutations do not agree).") 
   else if not (concl aconv (put_p (the p) prem)) 
-    then error "Eqvt lemma is not of the right form (arguments do not agree)"
+    then error (msg ^ "(arguments do not agree).")
   else 
     let
       val prem' = mk_perm (the p) prem    
@@ -173,7 +179,7 @@
       val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt
     in
       Goal.prove ctxt' [] [] goal'
-        (fn _ => eqvt_transform_imp_tac thy (the p) p' thm 1) 
+        (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) 
       |> singleton (ProofContext.export ctxt' ctxt)
       |> eqvt_transform_eq ctxt
     end