# HG changeset patch
# User wenzelm
# Date 1206814440 -3600
# Node ID 544cef16045b712b4d8664d9d8e747a9d4a03d4a
# Parent  3a2efce3e9925adf8be9ba2d63013dfc5f4e4e29
replaced 'ML_setup' by 'ML';

diff -r 3a2efce3e992 -r 544cef16045b doc-src/Locales/Locales/Locales.thy
--- a/doc-src/Locales/Locales/Locales.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/doc-src/Locales/Locales/Locales.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -398,7 +398,7 @@
   predicate is defined.
 *}
 (*<*)
-ML_setup {*
+ML {*
   val [comm_semi_ax1, comm_semi_ax2] = thms "comm_semi.axioms";
   bind_thm ("comm_semi_ax1", comm_semi_ax1);
   bind_thm ("comm_semi_ax2", comm_semi_ax2);
diff -r 3a2efce3e992 -r 544cef16045b src/CCL/Term.thy
--- a/src/CCL/Term.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/CCL/Term.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -220,7 +220,7 @@
 end
 *}
 
-ML_setup {*
+ML {*
 bind_thm ("ifBtrue", mk_beta_rl "if true then t else u = t");
 bind_thm ("ifBfalse", mk_beta_rl "if false then t else u = u");
 bind_thm ("ifBbot", mk_beta_rl "if bot then t else u = bot");
@@ -272,7 +272,7 @@
 
 subsection {* Constructors are injective *}
 
-ML_setup {*
+ML {*
 
 bind_thms ("term_injs", map (mk_inj_rl (the_context ())
   [thm "applyB", thm "splitB", thm "whenBinl", thm "whenBinr", thm "ncaseBsucc", thm "lcaseBcons"])
@@ -285,7 +285,7 @@
 
 subsection {* Constructors are distinct *}
 
-ML_setup {*
+ML {*
 bind_thms ("term_dstncts",
   mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs")
     [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
@@ -294,7 +294,7 @@
 
 subsection {* Rules for pre-order @{text "[="} *}
 
-ML_setup {*
+ML {*
 
 local
   fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
@@ -311,7 +311,7 @@
 
 subsection {* Rewriting and Proving *}
 
-ML_setup {*
+ML {*
   bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
 *}
 
diff -r 3a2efce3e992 -r 544cef16045b src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/FOLP/IFOLP.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -502,7 +502,7 @@
 
 (*special cases for free variables P, Q, R, S -- up to 3 arguments*)
 
-ML_setup {*
+ML {*
   bind_thms ("pred_congs",
     flat (map (fn c =>
                map (fn th => read_instantiate [("P",c)] th)
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -306,7 +306,7 @@
   end;
 *}
 
-ML_setup {* Addsimprocs [ring_simproc] *}
+ML {* Addsimprocs [ring_simproc] *}
 
 lemma natsum_ldistr:
   "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -282,7 +282,7 @@
   finally show ?thesis .
 qed
 
-(* ML_setup {* Addsimprocs [ring_simproc] *} *)
+(* ML {* Addsimprocs [ring_simproc] *} *)
 
 instance up :: (ring) ring
 proof
@@ -378,7 +378,7 @@
   qed
 qed
 *)
-ML_setup {* Delsimprocs [ring_simproc] *}
+ML {* Delsimprocs [ring_simproc] *}
 
 lemma monom_mult_is_smult:
   "monom (a::'a::ring) 0 * p = a *s p"
@@ -393,7 +393,7 @@
   then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
 qed
 
-ML_setup {* Addsimprocs [ring_simproc] *}
+ML {* Addsimprocs [ring_simproc] *}
 
 lemma monom_add [simp]:
   "monom (a + b) n = monom (a::'a::ring) n + monom b n"
@@ -442,14 +442,14 @@
 
 (* Polynomials form an algebra *)
 
-ML_setup {* Delsimprocs [ring_simproc] *}
+ML {* Delsimprocs [ring_simproc] *}
 
 lemma smult_assoc2:
   "(a *s p) * q = (a::'a::ring) *s (p * q)"
 by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
 (* Simproc fails. *)
 
-ML_setup {* Addsimprocs [ring_simproc] *}
+ML {* Addsimprocs [ring_simproc] *}
 
 (* the following can be derived from the above ones,
    for generality reasons, it is therefore done *)
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Bali/AxSem.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -1013,7 +1013,7 @@
 apply  (auto simp add: type_ok_def)
 done
 
-ML_setup {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
+ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
 declare ax_Abrupts [intro!]
 
 lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Bali/Eval.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -749,7 +749,7 @@
  29(AVar),24(Call)]
 *)
 
-ML_setup {*
+ML {*
 bind_thm ("eval_induct_", rearrange_prems 
 [0,1,2,8,4,30,31,27,15,16,
  17,18,19,20,21,3,5,25,26,23,6,
@@ -890,7 +890,7 @@
       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
     | _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *}
 
-ML_setup {*
+ML {*
 bind_thms ("AbruptIs", sum3_instantiate @{thm eval.Abrupt})
 *}
 
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Bali/Evaln.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -294,7 +294,7 @@
       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
     | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
 
-ML_setup {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
+ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *}
 declare evaln_AbruptIs [intro!]
 
 lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Bali/Example.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -894,7 +894,7 @@
 
 declare member_is_static_simp [simp]
 declare wt.Skip [rule del] wt.Init [rule del]
-ML_setup {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
+ML {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
 lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
 lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
 
@@ -1192,7 +1192,7 @@
 declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
         Base_foo_defs  [simp]
 
-ML_setup {* bind_thms ("eval_intros", map 
+ML {* bind_thms ("eval_intros", map 
         (simplify (@{simpset} delsimps @{thms Skip_eq}
                              addsimps @{thms lvar_def}) o 
          rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Bali/Term.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -266,7 +266,7 @@
   is_stmt :: "term \<Rightarrow> bool"
  "is_stmt t \<equiv> \<exists>c. t=In1r c"
 
-ML_setup {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
+ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
 
 declare is_stmt_rews [simp]
 
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/IntDiv.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -257,7 +257,7 @@
 
 text {* Tool setup *}
 
-ML_setup {*
+ML {*
 local 
 
 structure CancelDivMod = CancelDivModFun(
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/List.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -591,7 +591,7 @@
 - or both lists end in the same list.
 *}
 
-ML_setup {*
+ML {*
 local
 
 fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/OrderedGroup.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -1421,7 +1421,7 @@
 end);
 *}
 
-ML_setup {*
+ML {*
   Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
 *}
 
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Product_Type.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -57,7 +57,7 @@
   this rule directly --- it loops!
 *}
 
-ML_setup {*
+ML {*
   val unit_eq_proc =
     let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
       Simplifier.simproc @{theory} "unit_eq" ["x::unit"]
@@ -323,7 +323,7 @@
 
 lemmas split_tupled_all = split_paired_all unit_all_eq2
 
-ML_setup {*
+ML {*
   (* replace parameters of product type by individual component parameters *)
   val safe_full_simp_tac = generic_simp_tac true (true, false, false);
   local (* filtering with exists_paired_all is an essential optimization *)
@@ -429,7 +429,7 @@
   split_beta}.
 *}
 
-ML_setup {*
+ML {*
 
 local
   val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"]
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/Set.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -473,7 +473,7 @@
 lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
   by blast
 
-ML_setup {*
+ML {*
   local
     val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
     fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
diff -r 3a2efce3e992 -r 544cef16045b src/HOL/ex/Lagrange.thy
--- a/src/HOL/ex/Lagrange.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/ex/Lagrange.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -25,7 +25,7 @@
 
 (* These two simprocs are even less efficient than ordered rewriting
    and kill the second example: *)
-ML_setup {*
+ML {*
   Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
 *}
 
diff -r 3a2efce3e992 -r 544cef16045b src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOLCF/Pcpo.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -197,7 +197,7 @@
 lemma UU_reorient: "(\<bottom> = x) = (x = \<bottom>)"
 by auto
 
-ML_setup {*
+ML {*
 local
   val meta_UU_reorient = thm "UU_reorient" RS eq_reflection;
   fun reorient_proc sg _ (_ $ t $ u) =
diff -r 3a2efce3e992 -r 544cef16045b src/Sequents/Washing.thy
--- a/src/Sequents/Washing.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/Sequents/Washing.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -35,10 +35,10 @@
 
 (* "activate" definitions for use in proof *)
 
-ML_setup {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
-ML_setup {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
-ML_setup {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
-ML_setup {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
+ML {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
+ML {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
+ML {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
+ML {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
 
 (* a load of dirty clothes and two dollars gives you clean clothes *)
 
diff -r 3a2efce3e992 -r 544cef16045b src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/ZF/Datatype_ZF.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -12,7 +12,7 @@
 uses "Tools/datatype_package.ML"
 begin
 
-ML_setup {*
+ML {*
 (*Typechecking rules for most datatypes involving univ*)
 structure Data_Arg =
   struct
diff -r 3a2efce3e992 -r 544cef16045b src/ZF/Inductive_ZF.thy
--- a/src/ZF/Inductive_ZF.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/ZF/Inductive_ZF.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -41,7 +41,7 @@
 setup IndCases.setup
 setup DatatypeTactics.setup
 
-ML_setup {*
+ML {*
 structure Lfp =
   struct
   val oper      = @{const lfp}
diff -r 3a2efce3e992 -r 544cef16045b src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/ZF/OrdQuant.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -369,7 +369,7 @@
 
 text {* Setting up the one-point-rule simproc *}
 
-ML_setup {*
+ML {*
 local
 
 val unfold_rex_tac = unfold_tac [@{thm rex_def}];