# HG changeset patch
# User wenzelm
# Date 1205615246 -3600
# Node ID df8e5362cff9cd10ed40239e0994df30920d4b1c
# Parent  3ff5d257f1755e842adf8dbb91992eff864cc9a4
proper antiquotations;

diff -r 3ff5d257f175 -r df8e5362cff9 src/FOL/blastdata.ML
--- a/src/FOL/blastdata.ML	Sat Mar 15 22:07:25 2008 +0100
+++ b/src/FOL/blastdata.ML	Sat Mar 15 22:07:26 2008 +0100
@@ -1,14 +1,12 @@
-
-val ccontr = thm "ccontr";
 
 (*** Applying BlastFun to create Blast_tac ***)
 structure Blast_Data = 
   struct
   type claset	= Cla.claset
-  val equality_name = "op ="
-  val not_name = "Not"
-  val notE	= notE
-  val ccontr	= ccontr
+  val equality_name = @{const_name "op ="}
+  val not_name = @{const_name Not}
+  val notE	= @{thm notE}
+  val ccontr	= @{thm ccontr}
   val contr_tac = Cla.contr_tac
   val dup_intr	= Cla.dup_intr
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
diff -r 3ff5d257f175 -r df8e5362cff9 src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Sat Mar 15 22:07:25 2008 +0100
+++ b/src/FOL/cladata.ML	Sat Mar 15 22:07:26 2008 +0100
@@ -11,9 +11,9 @@
 (*** Applying ClassicalFun to create a classical prover ***)
 structure Classical_Data = 
   struct
-  val mp        = mp
-  val not_elim  = notE
-  val classical = thm "classical"
+  val mp        = @{thm mp}
+  val not_elim  = @{thm notE}
+  val classical = @{thm classical}
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
   end;
@@ -27,12 +27,13 @@
 
 (*Propositional rules*)
 val prop_cs = empty_cs
-  addSIs [refl, TrueI, conjI, thm "disjCI", impI, notI, iffI]
-  addSEs [conjE, disjE, thm "impCE", FalseE, thm "iffCE"];
+  addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI},
+    @{thm notI}, @{thm iffI}]
+  addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffCE}];
 
 (*Quantifier rules*)
-val FOL_cs = prop_cs addSIs [allI, thm "ex_ex1I"] addIs [exI]
-                     addSEs [exE, thm "alt_ex1E"] addEs [allE];
+val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
+                     addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
 
 val cla_setup = (fn thy => (change_claset_of thy (fn _ => FOL_cs); thy));
 
diff -r 3ff5d257f175 -r df8e5362cff9 src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Sat Mar 15 22:07:25 2008 +0100
+++ b/src/FOL/ex/Prolog.thy	Sat Mar 15 22:07:26 2008 +0100
@@ -63,7 +63,7 @@
 
 (*backtracking version*)
 ML {*
-val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (thms "rules") 1)
+val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (@{thms rules}) 1)
 *}
 
 lemma "rev(?x, a:b:c:Nil)"
@@ -76,13 +76,13 @@
 
 (*rev([a..p], ?w) requires 153 inferences *)
 lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
-apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})
+apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *})
 done
 
 (*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences
   total inferences = 2 + 1 + 17 + 561 = 581*)
 lemma "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"
-apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})
+apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *})
 done
 
 end
diff -r 3ff5d257f175 -r df8e5362cff9 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Mar 15 22:07:25 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Mar 15 22:07:26 2008 +0100
@@ -469,7 +469,7 @@
                    (*some risk of excessive simplification here -- might have
                      to identify the bare minimum set of rewrites*)
                    full_simp_tac
-                      (mut_ss addsimps conj_simps @ imp_simps @ quant_simps) 1
+                      (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1
                    THEN
                    (*unpackage and use "prem" in the corresponding place*)
                    REPEAT (rtac impI 1)  THEN
diff -r 3ff5d257f175 -r df8e5362cff9 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Sat Mar 15 22:07:25 2008 +0100
+++ b/src/ZF/Tools/typechk.ML	Sat Mar 15 22:07:26 2008 +0100
@@ -93,8 +93,8 @@
 fun typecheck_tac ctxt = REPEAT (typecheck_step_tac (tcset_of ctxt));
 
 (*Compiles a term-net for speed*)
-val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
-                                     @{thm ballI},allI,conjI,impI];
+val basic_res_tac = net_resolve_tac [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl},
+                                     @{thm ballI}, @{thm allI}, @{thm conjI}, @{thm impI}];
 
 (*Instantiates variables in typing conditions.
   drawback: does not simplify conjunctions*)
diff -r 3ff5d257f175 -r df8e5362cff9 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Sat Mar 15 22:07:25 2008 +0100
+++ b/src/ZF/arith_data.ML	Sat Mar 15 22:07:26 2008 +0100
@@ -130,7 +130,7 @@
 fun simplify_meta_eq rules =
   let val ss0 =
     FOL_ss addeqcongs [@{thm eq_cong2}, @{thm iff_cong2}]
-      delsimps iff_simps (*these could erase the whole rule!*)
+      delsimps @{thms iff_simps} (*these could erase the whole rule!*)
       addsimps rules
   in fn ss => mk_meta_eq o simplify (Simplifier.inherit_context ss ss0) end;