--- 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;