# HG changeset patch
# User wenzelm
# Date 1322431819 -3600
# Node ID cf10bde35973a8c0e4e20e6052e852eff46bc043
# Parent  63ed1be524eb6621c82453aefa24debc580d2198
more antiquotations;

diff -r 63ed1be524eb -r cf10bde35973 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/FOL/FOL.thy	Sun Nov 27 23:10:19 2011 +0100
@@ -337,12 +337,12 @@
 (*intuitionistic simprules only*)
 val IFOL_ss =
   FOL_basic_ss
-  addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
+  addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps}
   addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}]
   |> Simplifier.add_cong @{thm imp_cong};
 
 (*classical simprules too*)
-val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
+val FOL_ss = IFOL_ss addsimps @{thms cla_simps cla_ex_simps cla_all_simps};
 *}
 
 setup {* Simplifier.map_simpset_global (K FOL_ss) *}
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -19,7 +19,7 @@
 
 val nT = HOLogic.natT;
 val binarith = @{thms normalize_bin_simps};
-val comp_arith = binarith @ simp_thms
+val comp_arith = binarith @ @{thms simp_thms};
 
 val zdvd_int = @{thm zdvd_int};
 val zdiff_int_split = @{thm zdiff_int_split};
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -23,7 +23,7 @@
 val binarith =
   @{thms normalize_bin_simps} @ @{thms pred_bin_simps} @ @{thms succ_bin_simps} @
   @{thms add_bin_simps} @ @{thms minus_bin_simps} @  @{thms mult_bin_simps};
-val comp_arith = binarith @ simp_thms
+val comp_arith = binarith @ @{thms simp_thms};
 
 val zdvd_int = @{thm zdvd_int};
 val zdiff_int_split = @{thm zdiff_int_split};
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -163,7 +163,7 @@
                         qe))
                   [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
     val bex_conv =
-      Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)}))
+      Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms bex_simps(1-5)})
     val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
    in result_th
    end
@@ -200,8 +200,8 @@
  let
    val ss = simpset
    val ss' =
-     merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
-              @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss)
+     merge_ss (HOL_basic_ss addsimps @{thms simp_thms ex_simps all_simps
+                not_all all_not_ex ex_disj_distrib}, ss)
      |> Simplifier.inherit_context ss
    val pcv = Simplifier.rewrite ss'     
    val postcv = Simplifier.rewrite ss
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Decision_Procs/langford.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -26,7 +26,9 @@
                                      (Thm.cprop_of th), SOME x] th1) th
 in fold ins u th0 end;
 
-val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms))));
+val simp_rule =
+  Conv.fconv_rule
+    (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps @{thms ball_simps simp_thms})));
 
 fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = 
  case term_of ep of 
@@ -138,16 +140,14 @@
                  (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx))))
            |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
            |> Conv.fconv_rule (Conv.arg_conv 
-                   (Simplifier.rewrite 
-                      (HOL_basic_ss addsimps (simp_thms @ ex_simps))))
+                   (Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps})))
            |> SOME
           end
     | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
                  (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs))))
            |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
            |> Conv.fconv_rule (Conv.arg_conv 
-                   (Simplifier.rewrite 
-                (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) 
+                   (Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps})))
            |> SOME
    end
  | _ => NONE;
@@ -162,9 +162,9 @@
  let 
   val ss = dlo_ss addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc]
   val dnfex_conv = Simplifier.rewrite ss
-   val pcv = Simplifier.rewrite
-               (dlo_ss addsimps (simp_thms @ ex_simps @ all_simps)
-                @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib])
+  val pcv =
+    Simplifier.rewrite
+      (dlo_ss addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
  in fn p => 
    Qelim.gen_qelim_conv pcv pcv dnfex_conv cons 
                   (Thm.add_cterm_frees p [])  (K Thm.reflexive) (K Thm.reflexive)
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -37,7 +37,7 @@
              @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
              @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
              @{thm "diff_minus"}, @{thm "minus_divide_left"}]
-val comp_ths = ths @ comp_arith @ simp_thms 
+val comp_ths = ths @ comp_arith @ @{thms simp_thms};
 
 
 val zdvd_int = @{thm "zdvd_int"};
@@ -89,7 +89,7 @@
 
 fun mir_tac ctxt q = 
     Object_Logic.atomize_prems_tac
-        THEN' simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms)
+        THEN' simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
         THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
         THEN' SUBGOAL (fn (g, i) =>
   let
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOL.thy	Sun Nov 27 23:10:19 2011 +0100
@@ -2011,15 +2011,8 @@
   fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
 end;
 
-val all_conj_distrib = @{thm all_conj_distrib};
-val all_simps = @{thms all_simps};
-val atomize_not = @{thm atomize_not};
 val case_split = @{thm case_split};
-val cases_simp = @{thm cases_simp};
-val choice_eq = @{thm choice_eq};
 val cong = @{thm cong};
-val conj_comms = @{thms conj_comms};
-val conj_cong = @{thm conj_cong};
 val de_Morgan_conj = @{thm de_Morgan_conj};
 val de_Morgan_disj = @{thm de_Morgan_disj};
 val disj_assoc = @{thm disj_assoc};
@@ -2045,15 +2038,11 @@
 val imp_conjL = @{thm imp_conjL};
 val imp_conjR = @{thm imp_conjR};
 val imp_conv_disj = @{thm imp_conv_disj};
-val simp_implies_def = @{thm simp_implies_def};
-val simp_thms = @{thms simp_thms};
 val split_if = @{thm split_if};
 val the1_equality = @{thm the1_equality};
 val theI = @{thm theI};
 val theI' = @{thm theI'};
-val True_implies_equals = @{thm True_implies_equals};
-val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms @ @{thms "nnf_simps"})
-
+val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps});
 *}
 
 hide_const (open) eq equal
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -64,13 +64,13 @@
 
 (************************** miscellaneous functions ***************************)
 
-val simple_ss = HOL_basic_ss addsimps simp_thms
+val simple_ss = HOL_basic_ss addsimps @{thms simp_thms}
 
 val beta_rules =
   @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
   @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}
 
-val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules)
+val beta_ss = HOL_basic_ss addsimps (@{thms simp_thms} @ beta_rules)
 
 fun define_consts
     (specs : (binding * term * mixfix) list)
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -156,7 +156,7 @@
           fun con_thm p (con, args) =
             let
               val subgoal = con_assm false p (con, args)
-              val rules = prems @ con_rews @ simp_thms
+              val rules = prems @ con_rews @ @{thms simp_thms}
               val simplify = asm_simp_tac (HOL_basic_ss addsimps rules)
               fun arg_tac (lazy, _) =
                   rtac (if lazy then allI else case_UU_allI) 1
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -36,7 +36,7 @@
 struct
 
 val beta_ss =
-  HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}]
+  HOL_basic_ss addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}]
 
 fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo})
 
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -108,7 +108,7 @@
   }
 
 val beta_ss =
-  HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}]
+  HOL_basic_ss addsimps @{thms simp_thms} addsimprocs [@{simproc beta_cfun_proc}]
 
 (******************************************************************************)
 (******************************** theory data *********************************)
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Nov 27 23:10:19 2011 +0100
@@ -381,7 +381,7 @@
   @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
   @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
 
-val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
+val beta_ss = HOL_basic_ss addsimps (@{thms simp_thms} @ beta_rules);
 
 fun define_consts
     (specs : (binding * term * mixfix) list)
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Library/positivstellensatz.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -200,7 +200,7 @@
 val pth_square = @{lemma "x * x >= (0::real)"  by simp};
 
 val weak_dnf_simps =
-  List.take (simp_thms, 34) @
+  List.take (@{thms simp_thms}, 34) @
     @{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and
       "(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+};
 
@@ -351,7 +351,8 @@
        poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv,
        absconv1,absconv2,prover) = 
 let
- val pre_ss = HOL_basic_ss addsimps simp_thms@ ex_simps@ all_simps@[@{thm not_all},@{thm not_ex},ex_disj_distrib, all_conj_distrib, @{thm if_bool_eq_disj}]
+ val pre_ss = HOL_basic_ss addsimps
+  @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib all_conj_distrib if_bool_eq_disj}
  val prenex_ss = HOL_basic_ss addsimps prenex_simps
  val skolemize_ss = HOL_basic_ss addsimps [choice_iff]
  val presimp_conv = Simplifier.rewrite (Simplifier.context ctxt pre_ss)
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -1018,7 +1018,7 @@
             (fn _ =>
               simp_tac (HOL_basic_ss addsimps (supp_def ::
                  Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
-                 Collect_False_empty :: finite_emptyI :: simp_thms @
+                 Collect_False_empty :: finite_emptyI :: @{thms simp_thms} @
                  abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
         in
           (supp_thm,
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Prolog/prolog.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -62,7 +62,7 @@
   (Simplifier.global_context @{theory} empty_ss
     |> Simplifier.set_mksimps (mksimps mksimps_pairs))
   addsimps [
-        all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
+        @{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)" *)
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -38,7 +38,7 @@
 
 
 (** special setup for simpset **)
-val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
+val HOL_basic_ss' = HOL_basic_ss addsimps @{thms simp_thms Pair_eq}
   setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
   setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
 
@@ -206,7 +206,7 @@
         preds
   in 
     simp_tac (HOL_basic_ss addsimps
-      (@{thms HOL.simp_thms} @ (@{thm eval_pred} :: defs))) 1 
+      (@{thms HOL.simp_thms eval_pred} @ defs)) 1 
     (* need better control here! *)
   end
 
diff -r 63ed1be524eb -r cf10bde35973 src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Sun Nov 27 23:06:59 2011 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML	Sun Nov 27 23:10:19 2011 +0100
@@ -55,8 +55,7 @@
 local
 val pcv =
   Simplifier.rewrite
-    (HOL_basic_ss addsimps (@{thms simp_thms} @ @{thms ex_simps} @ @{thms all_simps} @
-        [@{thm all_not_ex}, not_all, @{thm ex_disj_distrib}]));
+    (HOL_basic_ss addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib});
 
 in fun standard_qelim_conv atcv ncv qcv p =
       gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p