--- a/Nominal-General/nominal_thmdecls.ML	Sun Apr 18 17:56:05 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Sun Apr 18 17:57:27 2010 +0200
@@ -33,6 +33,7 @@
   val setup: theory -> theory
   val get_eqvts_thms: Proof.context -> thm list
   val get_eqvts_raw_thms: Proof.context -> thm list
+  val eqvt_transform: Proof.context -> thm -> thm
 
   (* TEMPORARY FIX *)
   val add_thm: thm -> Context.generic -> Context.generic
@@ -87,12 +88,20 @@
 
 fun add_raw_thm thm = 
   case prop_of thm of
-    Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update (zero_var_indexes thm))
+    Const ("==", _) $ _ $ _ => 
+      EqvtRawData.map (Item_Net.update (zero_var_indexes thm))
   | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) 
 
 val del_raw_thm = EqvtRawData.map o Item_Net.remove;
 
-fun eq_transform_tac thm = 
+
+(** transformation of eqvt lemmas **)
+
+
+(* 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 = 
 let
   val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all}
 in
@@ -102,8 +111,7 @@
      rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
 end
 
-(* transform equations into the "p o c = c"-form *)
-fun transform_eq ctxt thm = 
+fun eqvt_transform_eq ctxt thm = 
 let
   val ((p, t), rhs) = apfst dest_perm 
     (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)))
@@ -118,18 +126,22 @@
   else if not (rhs aconv (put_p p t))
     then error "Eqvt lemma is not of the right form (arguments do not agree)"
   else if is_Const t 
-    then thm
+    then safe_mk_equiv thm
   else 
     let 
       val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
       val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
     in
-      Goal.prove ctxt [] [] goal' (fn _ => eq_transform_tac thm 1)
+      Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1)
       |> singleton (ProofContext.export ctxt' ctxt)
+      |> safe_mk_equiv
     end
 end
 
-fun imp_transform_tac thy p p' thm = 
+(* 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 = 
 let
   val cp = Thm.cterm_of thy p
   val cp' = Thm.cterm_of thy (mk_minus p')
@@ -140,7 +152,7 @@
     rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp]
 end
 
-fun transform_imp ctxt thm =
+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))
@@ -161,31 +173,46 @@
       val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt
     in
       Goal.prove ctxt' [] [] goal'
-        (fn _ => imp_transform_tac thy (the p) p' thm 1) 
+        (fn _ => eqvt_transform_imp_tac thy (the p) p' thm 1) 
       |> singleton (ProofContext.export ctxt' ctxt)
-      |> transform_eq ctxt
+      |> eqvt_transform_eq ctxt
     end
 end     
 
-fun transform addel_fun thm context = 
-let
-  val ctxt = Context.proof_of context
-in
-  case (prop_of thm) of
-    @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ 
-      (Const (@{const_name "permute"}, _) $ _ $ _) $ _) =>
-        addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context
-  | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => 
-        addel_fun (safe_mk_equiv (transform_imp ctxt thm)) context
-  | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
-end 
+fun eqvt_transform ctxt thm = 
+ case (prop_of thm) of
+   @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ 
+     (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => 
+       eqvt_transform_eq ctxt thm
+ | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => 
+     eqvt_transform_imp ctxt thm
+ | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
+ 
+
+(** attributes **)
 
-val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm));
-val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm));
+val eqvt_add = Thm.declaration_attribute 
+  (fn thm => fn context =>
+   let
+     val thm' = eqvt_transform (Context.proof_of context) thm
+   in
+     context |> add_thm thm |> add_raw_thm thm'
+   end)
+
+val eqvt_del = Thm.declaration_attribute
+  (fn thm => fn context =>
+   let
+     val thm' = eqvt_transform (Context.proof_of context) thm
+   in
+     context |> del_thm thm |> del_raw_thm thm'
+   end)
 
 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;
 val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;
 
+
+(** setup function **)
+
 val setup =
   Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) 
     (cat_lines ["Declaration of equivariance lemmas - they will automtically be",