# HG changeset patch
# User wenzelm
# Date 1205962097 -3600
# Node ID f8ed02f224335dc00070d028875fd390ea3e1755
# Parent  44473c957672bb6b15a5171e07a1ee9e270fc592
auxiliary dynamic_thm(s) for fact lookup;
renamed local dynamic_thm(s) to goal_thm(s);

diff -r 44473c957672 -r f8ed02f22433 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Wed Mar 19 22:28:08 2008 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Mar 19 22:28:17 2008 +0100
@@ -71,8 +71,8 @@
 val supports_fresh_rule = @{thm "supports_fresh"};
 
 (* pulls out dynamically a thm via the proof state *)
-fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
-fun dynamic_thm  st name = PureThy.get_thm  (theory_of_thm st) (Name name);
+fun global_thms st name = PureThy.get_thms (theory_of_thm st) (Facts.Named (name, NONE));
+fun global_thm  st name = PureThy.get_thm  (theory_of_thm st) (Facts.Named (name, NONE));
 
 
 (* needed in the process of fully simplifying permutations *)
@@ -111,8 +111,8 @@
             (if (applicable_app f) then
               let
                 val name = Sign.base_name n
-                val at_inst = PureThy.get_thm sg (Name ("at_" ^ name ^ "_inst"))
-                val pt_inst = PureThy.get_thm sg (Name ("pt_" ^ name ^ "_inst"))
+                val at_inst = dynamic_thm sg ("at_" ^ name ^ "_inst")
+                val pt_inst = dynamic_thm sg ("pt_" ^ name ^ "_inst")
               in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
             else NONE)
       | _ => NONE
@@ -146,7 +146,7 @@
     ("general simplification of permutations", fn st =>
     let
        val ss' = Simplifier.theory_context (theory_of_thm st) ss
-         addsimps ((List.concat (map (dynamic_thms st) dyn_thms))@eqvt_thms)
+         addsimps ((List.concat (map (global_thms st) dyn_thms))@eqvt_thms)
          delcongs weak_congs
          addcongs strong_congs
          addsimprocs [perm_simproc_fun, perm_simproc_app]
@@ -198,13 +198,13 @@
           SOME (Drule.instantiate'
             [SOME (ctyp_of sg (fastype_of t))]
             [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
-            (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
-             PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose_aux)))
+            (mk_meta_eq ([dynamic_thm sg ("pt_"^tname'^"_inst"),
+             dynamic_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
         else
           SOME (Drule.instantiate'
             [SOME (ctyp_of sg (fastype_of t))]
             [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
-            (mk_meta_eq (PureThy.get_thm sg (Name ("cp_"^tname'^"_"^uname'^"_inst")) RS 
+            (mk_meta_eq (dynamic_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS 
              cp1_aux)))
       else NONE
     end
@@ -307,7 +307,7 @@
               Logic.strip_assums_concl (hd (prems_of supports_rule'));
             val supports_rule'' = Drule.cterm_instantiate
               [(cert (head_of S), cert s')] supports_rule'
-            val fin_supp = dynamic_thms st ("fin_supp")
+            val fin_supp = global_thms st ("fin_supp")
             val ss' = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
           in
             (tactical ("guessing of the right supports-set",
@@ -326,8 +326,8 @@
 fun fresh_guess_tac tactical ss i st =
     let 
 	val goal = List.nth(cprems_of st, i-1)
-        val fin_supp = dynamic_thms st ("fin_supp")
-        val fresh_atm = dynamic_thms st ("fresh_atm")
+        val fin_supp = global_thms st ("fin_supp")
+        val fresh_atm = global_thms st ("fresh_atm")
 	val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
         val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
     in