src/HOL/Nominal/nominal_thmdecls.ML

--- a/src/HOL/Nominal/nominal_thmdecls.ML	Mon Apr 02 11:31:08 2007 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Mon Apr 02 23:24:52 2007 +0200
@@ -2,7 +2,7 @@
    Authors: Julien Narboux and Christian Urban
 
    This file introduces the infrastructure for the lemma 
-   declaration "eqvt" "bij" and "fresh".
+   declaration "eqvts" "bijs" and "freshs".
 
    By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored 
    in a data-slot in the theory context. Possible modifiers
@@ -30,12 +30,12 @@
 structure Data = GenericDataFun
 (
   val name = "HOL/Nominal/eqvt";
-  type T = {eqvts:thm list, fresh:thm list, bij:thm list};
-  val empty = ({eqvts=[], fresh=[], bij=[]}:T);
+  type T = {eqvts:thm list, freshs:thm list, bijs:thm list};
+  val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
   val extend = I;
   fun merge _ (r1:T,r2:T) = {eqvts  = Drule.merge_rules (#eqvts r1, #eqvts r2), 
-                             fresh = Drule.merge_rules (#fresh r1, #fresh r2), 
-                             bij   = Drule.merge_rules (#bij r1, #bij r2)}
+                             freshs = Drule.merge_rules (#freshs r1, #freshs r2), 
+                             bijs   = Drule.merge_rules (#bijs r1, #bijs r2)}
   fun print context (data:T) =
     let 
        fun print_aux msg thms =
@@ -43,8 +43,8 @@
            (map (ProofContext.pretty_thm (Context.proof_of context)) thms))
     in
       (print_aux "Equivariance lemmas: " (#eqvts data);
-       print_aux "Freshness lemmas: " (#fresh data);
-       print_aux "Bijection lemmas: " (#bij data))
+       print_aux "Freshness lemmas: " (#freshs data);
+       print_aux "Bijection lemmas: " (#bijs data))
     end;
  
 );
@@ -62,8 +62,8 @@
 
 val print_data = Data.print o Context.Proof;
 val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts;
-val get_fresh_thms = Context.Theory #> Data.get #> #fresh;
-val get_bij_thms = Context.Theory #> Data.get #> #bij;
+val get_fresh_thms = Context.Theory #> Data.get #> #freshs;
+val get_bij_thms = Context.Theory #> Data.get #> #bijs;
 
 (* FIXME: should be a function in a library *)
 fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
@@ -195,13 +195,13 @@
      Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context' 
    end
 
-fun bij_add_del_aux f   = simple_add_del_aux #bij "bij" f
-fun fresh_add_del_aux f = simple_add_del_aux #fresh "fresh" f
+fun bij_add_del_aux f   = simple_add_del_aux #bijs "bijs" f
+fun fresh_add_del_aux f = simple_add_del_aux #freshs "freshs" f
 fun eqvt_force_add_del_aux f = simple_add_del_aux #eqvts "eqvts" f
 
-fun eqvt_map f th (r:Data.T)  = {eqvts = (f th (#eqvts r)), fresh = #fresh r, bij = #bij r};
-fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, fresh = (f th (#fresh r)), bij = #bij r};
-fun bij_map f th (r:Data.T)   = {eqvts = #eqvts r, fresh = #fresh r, bij = (f th (#bij r))};
+fun eqvt_map f th (r:Data.T)  = {eqvts = (f th (#eqvts r)), freshs = #freshs r, bijs = #bijs r};
+fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r};
+fun bij_map f th (r:Data.T)   = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))};
 
 val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); 
 val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));