# HG changeset patch
# User wenzelm
# Date 1206478788 -3600
# Node ID 2f0500e375fe2267fbe2d19e83ec0ef7ab299dfd
# Parent  c08a5ab37fcd3cd29539e8939b1f6adedb06eaba
update_context: always store as "Nominal.eqvts";
added dynamic fact bindings for "eqvts", "freshs", "bijs";

diff -r c08a5ab37fcd -r 2f0500e375fe src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Tue Mar 25 21:47:19 2008 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Tue Mar 25 21:59:48 2008 +0100
@@ -108,9 +108,12 @@
 fun update_context flag thms context =
   let
      val context' = fold (fn thm => Data.map (flag thm)) thms context
-  in
-    Context.mapping (snd o PureThy.add_thmss [(("eqvts",(#eqvts (Data.get context'))),[])]) I context'
-  end;
+     fun update_eqvts thy = thy
+       |> Sign.root_path
+       |> Sign.add_path "Nominal"
+       |> (snd o PureThy.add_thmss [(("eqvts", (#eqvts (Data.get context'))), [])])
+       |> Sign.restore_naming thy;
+  in Context.mapping update_eqvts I context' end;
 
 (* replaces every variable x in t with pi o x *)
 fun apply_pi trm (pi,typi) =
@@ -220,6 +223,9 @@
       ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
         "equivariance theorem declaration (without checking the form of the lemma)"),
       ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
-      ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")];
+      ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")] #>
+  PureThy.add_thms_dynamic ("eqvts", #eqvts o Data.get) #>
+  PureThy.add_thms_dynamic ("freshs", #freshs o Data.get) #>
+  PureThy.add_thms_dynamic ("bijs", #bijs o Data.get);
 
 end;