# HG changeset patch
# User urbanc
# Date 1188729260 -7200
# Node ID 5c435b2ea13760f5411815f0d4cae9999d994fd5
# Parent  4dd086997bab2ec03b0046f398913ece652e89b9
made theorem-references safe

diff -r 4dd086997bab -r 5c435b2ea137 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Sat Sep 01 18:17:44 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Sun Sep 02 12:34:20 2007 +0200
@@ -49,23 +49,23 @@
 struct
 
 (* some lemmas needed below *)
-val finite_emptyI = thm "finite.emptyI";
-val finite_Un     = thm "finite_Un";
-val conj_absorb   = thm "conj_absorb";
-val not_false     = thm "not_False_eq_True"
-val perm_fun_def  = thm "Nominal.perm_fun_def"
-val perm_eq_app   = thm "Nominal.pt_fun_app_eq"
-val supports_def  = thm "Nominal.supports_def";
-val fresh_def     = thm "Nominal.fresh_def";
-val fresh_prod    = thm "Nominal.fresh_prod";
-val fresh_unit    = thm "Nominal.fresh_unit";
-val supports_rule = thm "supports_finite";
-val supp_prod     = thm "supp_prod";
-val supp_unit     = thm "supp_unit";
-val pt_perm_compose_aux = thm "pt_perm_compose_aux";
-val cp1_aux             = thm "cp1_aux";
-val perm_aux_fold       = thm "perm_aux_fold"; 
-val supports_fresh_rule = thm "supports_fresh";
+val finite_emptyI = @{thm "finite.emptyI"};
+val finite_Un     = @{thm "finite_Un"};
+val conj_absorb   = @{thm "conj_absorb"};
+val not_false     = @{thm "not_False_eq_True"}
+val perm_fun_def  = @{thm "Nominal.perm_fun_def"};
+val perm_eq_app   = @{thm "Nominal.pt_fun_app_eq"};
+val supports_def  = @{thm "Nominal.supports_def"};
+val fresh_def     = @{thm "Nominal.fresh_def"};
+val fresh_prod    = @{thm "Nominal.fresh_prod"};
+val fresh_unit    = @{thm "Nominal.fresh_unit"};
+val supports_rule = @{thm "supports_finite"};
+val supp_prod     = @{thm "supp_prod"};
+val supp_unit     = @{thm "supp_unit"};
+val pt_perm_compose_aux = @{thm "pt_perm_compose_aux"};
+val cp1_aux             = @{thm "cp1_aux"};
+val perm_aux_fold       = @{thm "perm_aux_fold"}; 
+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);
@@ -73,12 +73,12 @@
 
 
 (* needed in the process of fully simplifying permutations *)
-val strong_congs = [thm "if_cong"]
+val strong_congs = [@{thm "if_cong"}]
 (* needed to avoid warnings about overwritten congs *)
-val weak_congs   = [thm "if_weak_cong"]
+val weak_congs   = [@{thm "if_weak_cong"}]
 
+(* FIXME comment *)
 (* a tactical which fails if the tactic taken as an argument generates does not solve the sub goal i *)
-
 fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac);
 
 (* debugging *)
@@ -115,7 +115,7 @@
       | _ => NONE
   end
 
-(* a simproc that deals with instances in front of functions  *)
+(* a simproc that deals with permutation instances in front of functions  *)
 fun perm_simproc_fun st sg ss redex = 
    let 
      fun applicable_fun t =
@@ -235,13 +235,9 @@
 (*     pi o f = rhs                           *)  
 (* is transformed to                          *)
 (*     %x. pi o (f ((rev pi) o x)) = rhs      *)
-fun unfold_perm_fun_def_tac i = 
-    let
-	val perm_fun_def = thm "Nominal.perm_fun_def"
-    in
-	("unfolding of permutations on functions", 
-         rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
-    end
+fun unfold_perm_fun_def_tac i =
+    ("unfolding of permutations on functions", 
+      rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
 
 (* applies the ext-rule such that      *)
 (*                                     *)