--- a/Quot/Nominal/Nominal2_Eqvt.thy	Thu Feb 04 17:39:04 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy	Fri Feb 05 09:06:27 2010 +0100
@@ -226,6 +226,8 @@
 use "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
 
+
+
 lemmas [eqvt] = 
   (* connectives *)
   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
@@ -233,8 +235,7 @@
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  permute_eqvt supp_eqvt fresh_eqvt
-  permute_pure
+  supp_eqvt fresh_eqvt permute_pure
 
   (* datatypes *)
   permute_prod.simps
@@ -244,6 +245,8 @@
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
   Diff_eqvt Compl_eqvt insert_eqvt
 
+lemmas [eqvt_raw] = permute_eqvt
+
 thm eqvts
 thm eqvts_raw
 

--- a/Quot/Nominal/nominal_permeq.ML	Thu Feb 04 17:39:04 2010 +0100
+++ b/Quot/Nominal/nominal_permeq.ML	Fri Feb 05 09:06:27 2010 +0100
@@ -59,7 +59,7 @@
         then_conv Conv.comb_conv (eqvt_conv ctxt),
       eqvt_lambda_conv ctxt
         then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt,
-      More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvt_raw_thms ctxt),
+      More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt),
       Conv.all_conv
     ] ct
 

--- a/Quot/Nominal/nominal_thmdecls.ML	Thu Feb 04 17:39:04 2010 +0100
+++ b/Quot/Nominal/nominal_thmdecls.ML	Fri Feb 05 09:06:27 2010 +0100
@@ -3,18 +3,18 @@
 
   Infrastructure for the lemma collection "eqvts".
 
-  Provides the attributes [eqvt] and [eqvt_force], and the theorem
-  lists eqvts and eqvts_raw. The first attribute will store the theorem
-  in the eqvts list and also in the eqvts_raw list. For the latter 
-  the theorem is expected to be of the form
+  Provides the attributes [eqvt] and [eqvt_raw], and the theorem
+  lists eqvts and eqvts_raw. The first attribute will store the 
+  theorem in the eqvts list and also in the eqvts_raw list. For 
+  the latter the theorem is expected to be of the form
 
     p o (c x1 x2 ...) = c (p o x1) (p o x2) ...
 
-  and is stored in the form
+  and it is stored in the form
 
     p o c == c
 
-  The [eqvt_force] attribute just adds the theorem to eqvts.
+  The [eqvt_raw] attribute just adds the theorem to eqvts_raw.
 
   TODO:
 
@@ -27,36 +27,41 @@
 sig
   val eqvt_add: attribute
   val eqvt_del: attribute
-  val eqvt_force_add: attribute
-  val eqvt_force_del: attribute
+  val eqvt_raw_add: attribute
+  val eqvt_raw_del: attribute
   val setup: theory -> theory
-  val get_eqvt_thms: Proof.context -> thm list
-  val get_eqvt_raw_thms: Proof.context -> thm list
+  val get_eqvts_thms: Proof.context -> thm list
+  val get_eqvts_raw_thms: Proof.context -> thm list
 
 end;
 
 structure Nominal_ThmDecls: NOMINAL_THMDECLS =
 struct
 
+
 structure EqvtData = Generic_Data
-(
-  type T = (thm * thm option) Item_Net.T;
-  val empty = Item_Net.init (eq_fst Thm.eq_thm_prop) (single o Thm.full_prop_of o fst)
+( type T = thm Item_Net.T;
+  val empty = Thm.full_rules;
   val extend = I;
-  val merge = Item_Net.merge;
-);
+  val merge = Item_Net.merge );
 
-val eqvts = (map fst) o Item_Net.content o EqvtData.get;
-val eqvts_raw = (map_filter snd) o Item_Net.content o EqvtData.get;
+structure EqvtRawData = Generic_Data
+( type T = thm Item_Net.T;
+  val empty = Thm.full_rules;
+  val extend = I;
+  val merge = Item_Net.merge );
 
-val get_eqvt_thms = eqvts o Context.Proof; 
-val get_eqvt_raw_thms = eqvts_raw o Context.Proof; 
+val eqvts = Item_Net.content o EqvtData.get;
+val eqvts_raw = Item_Net.content o EqvtRawData.get;
+
+val get_eqvts_thms = eqvts o Context.Proof; 
+val get_eqvts_raw_thms = eqvts_raw o Context.Proof; 
 
 val add_thm = EqvtData.map o Item_Net.update;
 val del_thm = EqvtData.map o Item_Net.remove;
 
-val add_force_thm = EqvtData.map o Item_Net.update;
-val del_force_thm = EqvtData.map o Item_Net.remove;
+val add_raw_thm = EqvtRawData.map o Item_Net.update;
+val del_raw_thm = EqvtRawData.map o Item_Net.remove;
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM("dest_perm", [t])
@@ -94,7 +99,7 @@
     (fn _ => eqvt_transform_tac thm 1)
 end
 
-fun transform addel_fn thm context = 
+fun transform addel_fun thm context = 
 let
   val ctxt = Context.proof_of context
   val trm = HOLogic.dest_Trueprop (prop_of thm)
@@ -102,27 +107,28 @@
   case trm of
     Const (@{const_name "op ="}, _) $ lhs $ rhs =>
       let 
-        val thm2 = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}
+        val thm' = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}
       in
-        addel_fn (thm, SOME thm2) context
+        addel_fun thm' context
       end
   | _ => raise (error "only (op=) case implemented yet")
 end 
 
-val eqvt_add = Thm.declaration_attribute (transform add_thm);
-val eqvt_del = Thm.declaration_attribute (transform del_thm);
+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_force_add = Thm.declaration_attribute (add_force_thm o rpair NONE);
-val eqvt_force_del = Thm.declaration_attribute (del_force_thm o rpair NONE);
+val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;
+val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;
 
 val setup =
   Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) 
     (cat_lines ["declaration of equivariance lemmas - they will automtically be",  
        "brought into the form p o c = c"]) #>
-  Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) 
+  Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) 
     (cat_lines ["declaration of equivariance lemmas - no",
        "transformation is performed"]) #>
   PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
   PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);
 
+
 end;