# HG changeset patch
# User wenzelm
# Date 1326130182 -3600
# Node ID 4ed94d92ae19048e1db4032c73ceea2f4f09c95b
# Parent  f363e5a2f8e810e599780f3032be99b4fce1c549
prefer antiquotations;

diff -r f363e5a2f8e8 -r 4ed94d92ae19 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Jan 09 14:47:18 2012 +0100
+++ b/src/HOL/HOL.thy	Mon Jan 09 18:29:42 2012 +0100
@@ -2008,37 +2008,6 @@
   fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
 end;
 
-val case_split = @{thm case_split};
-val cong = @{thm cong};
-val de_Morgan_conj = @{thm de_Morgan_conj};
-val de_Morgan_disj = @{thm de_Morgan_disj};
-val disj_assoc = @{thm disj_assoc};
-val disj_comms = @{thms disj_comms};
-val disj_cong = @{thm disj_cong};
-val eq_ac = @{thms eq_ac};
-val eq_cong2 = @{thm eq_cong2}
-val Eq_FalseI = @{thm Eq_FalseI};
-val Eq_TrueI = @{thm Eq_TrueI};
-val Ex1_def = @{thm Ex1_def};
-val ex_disj_distrib = @{thm ex_disj_distrib};
-val ex_simps = @{thms ex_simps};
-val if_cancel = @{thm if_cancel};
-val if_eq_cancel = @{thm if_eq_cancel};
-val if_False = @{thm if_False};
-val iff_conv_conj_imp = @{thm iff_conv_conj_imp};
-val iff = @{thm iff};
-val if_splits = @{thms if_splits};
-val if_True = @{thm if_True};
-val if_weak_cong = @{thm if_weak_cong};
-val imp_all = @{thm imp_all};
-val imp_cong = @{thm imp_cong};
-val imp_conjL = @{thm imp_conjL};
-val imp_conjR = @{thm imp_conjR};
-val imp_conv_disj = @{thm imp_conv_disj};
-val split_if = @{thm split_if};
-val the1_equality = @{thm the1_equality};
-val theI = @{thm theI};
-val theI' = @{thm theI'};
 val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps});
 *}
 
diff -r f363e5a2f8e8 -r 4ed94d92ae19 src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Jan 09 14:47:18 2012 +0100
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Jan 09 18:29:42 2012 +0100
@@ -121,7 +121,7 @@
 local
   fun solve_cont thy _ t =
     let
-      val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI
+      val tr = instantiate' [] [SOME (cterm_of thy t)] @{thm Eq_TrueI}
     in Option.map fst (Seq.pull (cont_tac 1 tr)) end
 in
   fun cont_proc thy =
diff -r f363e5a2f8e8 -r 4ed94d92ae19 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon Jan 09 14:47:18 2012 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Jan 09 18:29:42 2012 +0100
@@ -982,7 +982,7 @@
                  else foldr1 (HOLogic.mk_binop @{const_abbrev union}) (map supp args2)))))
             (fn _ =>
               simp_tac (HOL_basic_ss addsimps (supp_def ::
-                 Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
+                 Un_assoc :: @{thm de_Morgan_conj} :: Collect_disj_eq :: finite_Un ::
                  Collect_False_empty :: finite_emptyI :: @{thms simp_thms} @
                  abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
         in
@@ -1968,7 +1968,7 @@
                   end) context 1])) idxss) (ndescr ~~ rec_elims))
          end));
 
-    val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
+    val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
 
     (* define primrec combinators *)
 
@@ -2011,7 +2011,7 @@
           (augment_sort thy12 fs_cp_sort concl')
           (fn {prems, ...} => EVERY
             [rewrite_goals_tac reccomb_defs,
-             rtac the1_equality 1,
+             rtac @{thm the1_equality} 1,
              solve rec_unique_thms prems 1,
              resolve_tac rec_intrs 1,
              REPEAT (solve (prems @ rec_total_thms) prems 1)])
diff -r f363e5a2f8e8 -r 4ed94d92ae19 src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Mon Jan 09 14:47:18 2012 +0100
+++ b/src/HOL/Prolog/prolog.ML	Mon Jan 09 18:29:42 2012 +0100
@@ -63,9 +63,9 @@
     |> Simplifier.set_mksimps (mksimps mksimps_pairs))
   addsimps [
         @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
-        imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
-        imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
-        imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
+        @{thm imp_conjL} RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
+        @{thm imp_conjR},        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
+        @{thm imp_all}];         (* "((!x. D) :- G) = (!x. D :- G)" *)
 
 
 (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>