# HG changeset patch
# User wenzelm
# Date 1185648022 -7200
# Node ID 67bde7cfcf10e09ed5233d60da154cd8708b0aec
# Parent  edd20fe274b510f697537b2be3f39b91de94b381
tuned ML/simproc declarations;

diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/AxSem.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -471,10 +471,8 @@
 declare split_paired_All [simp del] split_paired_Ex [simp del] 
 declare split_if     [split del] split_if_asm     [split del] 
         option.split [split del] option.split_asm [split del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-change_claset (fn cs => cs delSWrapper "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
 
 inductive
   ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
@@ -1015,9 +1013,7 @@
 apply  (auto simp add: type_ok_def)
 done
 
-ML {*
-bind_thms ("ax_Abrupts", sum3_instantiate (thm "ax_derivs.Abrupt"))
-*}
+ML_setup {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
 declare ax_Abrupts [intro!]
 
 lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/AxSound.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -210,9 +210,7 @@
 done
   
 
-
-
-ML "Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]"
+declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]]
 
 lemma valid_stmtI: 
    assumes I: "\<And> n s0 L accC C s1 Y Z.
diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/Basis.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -11,22 +11,13 @@
 Unify.search_bound := 40;
 Unify.trace_bound  := 40;
 *}
-(*print_depth 100;*)
-(*Syntax.ambiguity_level := 1;*)
 
 section "misc"
 
 declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
 
-ML {*
-fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.theory_of_thm thm) name [pat]
-  (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm));
-*}
-
 declare split_if_asm  [split] option.split [split] option.split_asm [split]
-ML {*
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 declare if_weak_cong [cong del] option.weak_case_cong [cong del]
 declare length_Suc_conv [iff]
 
diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -820,9 +820,8 @@
 declare inj_term_sym_simps [simp]
 declare assigns_if.simps [simp del]
 declare split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+
 inductive_cases da_elim_cases [cases set]:
   "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" 
   "Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A" 
@@ -887,9 +886,8 @@
 declare inj_term_sym_simps [simp del]
 declare assigns_if.simps [simp]
 declare split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
+
 (* To be able to eliminate both the versions with the overloaded brackets: 
    (B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A), 
    every rule appears in both versions
diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -4,9 +4,7 @@
 
 theory DefiniteAssignmentCorrect imports WellForm Eval begin
 
-ML {*
-Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
-*}
+declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
 
 lemma sxalloc_no_jump:
   assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and
@@ -4496,7 +4494,6 @@
     using that by (rule da_good_approxE) iprover+
 qed
 
-ML {*
-Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
-*}
+declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]]
+
 end
diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/Eval.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -749,12 +749,12 @@
  29(AVar),24(Call)]
 *)
 
-ML {*
+ML_setup {*
 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,
  7,11,9,13,14,12,22,10,28,
- 29,24] (thm "eval.induct"))
+ 29,24] @{thm eval.induct})
 *}
 
 
@@ -790,9 +790,8 @@
 
 declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
 declare split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+
 inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
 
 inductive_cases eval_elim_cases [cases set]:
@@ -829,9 +828,7 @@
 	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> (x, s')"
 declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
 declare split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 declare split_if     [split] split_if_asm     [split] 
         option.split [split] option.split_asm [split]
 
@@ -869,25 +866,35 @@
 lemma eval_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<rightarrow> s')"
   by (auto, frule eval_Inj_elim, auto, frule eval_Inj_elim, auto)
 
+simproc_setup eval_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+    | _ => SOME (mk_meta_eq @{thm eval_expr_eq})) *}
+
+simproc_setup eval_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+    | _ => SOME (mk_meta_eq @{thm eval_var_eq})) *}
+
+simproc_setup eval_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+    | _ => SOME (mk_meta_eq @{thm eval_exprs_eq})) *}
+
+simproc_setup eval_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+    | _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *}
+
 ML_setup {*
-fun eval_fun name lhs =
-let
-  fun is_Inj (Const (inj,_) $ _) = true
-    | is_Inj _                   = false
-  fun pred (_ $ _ $ _ $ _ $ x $ _) = is_Inj x
-in
-  cond_simproc name lhs pred (thm name)
-end
-
-val eval_expr_proc  = eval_fun "eval_expr_eq"  "G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')";
-val eval_var_proc   = eval_fun "eval_var_eq"   "G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')";
-val eval_exprs_proc = eval_fun "eval_exprs_eq" "G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')";
-val eval_stmt_proc  = eval_fun "eval_stmt_eq"  "G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')";
-Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
-bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))
+bind_thms ("AbruptIs", sum3_instantiate @{thm eval.Abrupt})
 *}
 
-declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!] 
+declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!]
 
 text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only
 used in smallstep semantics, not in the bigstep semantics. So their is no
@@ -955,17 +962,11 @@
 apply (frule eval_no_abrupt_lemma, auto)+
 done
 
-ML {*
-local
-  fun is_None (Const ("Datatype.option.None",_)) = true
-    | is_None _ = false
-  fun pred (_ $ _ $ (Const ("Pair", _) $ x $ _) $ _  $ _ $ _) = is_None x
-in
-  val eval_no_abrupt_proc = 
-  cond_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 
-          (thm "eval_no_abrupt")
-end;
-Addsimprocs [eval_no_abrupt_proc]
+simproc_setup eval_no_abrupt ("G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ (Const ("Pair", _) $ (Const ("Datatype.option.None",_)) $ _) $ _  $ _ $ _) => NONE
+    | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))
 *}
 
 
@@ -981,17 +982,11 @@
 apply (frule eval_abrupt_lemma, auto)+
 done
 
-ML {*
-local
-  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
-    | is_Some _ = false
-  fun pred (_ $ _ $ _ $ _ $ _ $ x) = is_Some x
-in
-  val eval_abrupt_proc = 
-  cond_simproc "eval_abrupt" 
-               "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
-end;
-Addsimprocs [eval_abrupt_proc]
+simproc_setup eval_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ _ $ (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _)) => NONE
+    | _ => SOME (mk_meta_eq @{thm eval_abrupt}))
 *}
 
 
diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/Evaln.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -198,9 +198,8 @@
         option.split [split del] option.split_asm [split del]
         not_None_eq [simp del] 
         split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+
 inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
 
 inductive_cases evaln_elim_cases:
@@ -241,9 +240,8 @@
         option.split [split] option.split_asm [split]
         not_None_eq [simp] 
         split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
+
 lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
   (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
   | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
@@ -272,24 +270,31 @@
 lemma evaln_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<midarrow>n\<rightarrow> s')"
   by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
 
-ML_setup {*
-fun enf name lhs =
-let
-  fun is_Inj (Const (inj,_) $ _) = true
-    | is_Inj _                   = false
-  fun pred (_ $ _ $ _ $ _ $ _ $ x $ _) = is_Inj x
-in
-  cond_simproc name lhs pred (thm name)
-end;
+simproc_setup evaln_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+    | _ => SOME (mk_meta_eq @{thm evaln_expr_eq})) *}
+
+simproc_setup evaln_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+    | _ => SOME (mk_meta_eq @{thm evaln_var_eq})) *}
 
-val evaln_expr_proc  = enf "evaln_expr_eq"  "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')";
-val evaln_var_proc   = enf "evaln_var_eq"   "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
-val evaln_exprs_proc = enf "evaln_exprs_eq" "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
-val evaln_stmt_proc  = enf "evaln_stmt_eq"  "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')";
-Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
+simproc_setup evaln_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+    | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq})) *}
 
-bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
-*}
+simproc_setup evaln_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
+    | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
+
+ML_setup {* 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"
@@ -352,16 +357,12 @@
 apply (frule evaln_abrupt_lemma, auto)+
 done
 
-ML {*
-local
-  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
-    | is_Some _ = false
-  fun pred (_ $ _ $ _ $ _ $ _ $ _ $ x) = is_Some x
-in
-  val evaln_abrupt_proc = 
- cond_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
-end;
-Addsimprocs [evaln_abrupt_proc]
+simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ _ $ _ $ (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _))
+        => NONE
+    | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
 *}
 
 lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
@@ -509,9 +510,7 @@
   show ?thesis .
 qed
 
-ML {*
-Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
-*}
+declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
 
 section {* eval implies evaln *}
 lemma eval_evaln: 
diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/Example.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -894,7 +894,7 @@
 
 declare member_is_static_simp [simp]
 declare wt.Skip [rule del] wt.Init [rule del]
-ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
+ML_setup {* 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,10 +1192,10 @@
 declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
         Base_foo_defs  [simp]
 
-ML {* bind_thms ("eval_intros", map 
-        (simplify (simpset() delsimps [thm "Skip_eq"]
-                             addsimps [thm "lvar_def"]) o 
-         rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
+ML_setup {* 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}) *}
 lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
 
 consts
diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/Term.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -266,9 +266,7 @@
   is_stmt :: "term \<Rightarrow> bool"
  "is_stmt t \<equiv> \<exists>c. t=In1r c"
 
-ML {*
-bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
-*}
+ML_setup {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
 
 declare is_stmt_rews [simp]
 
diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -733,10 +733,9 @@
 declare split_paired_All [simp del] split_paired_Ex [simp del] 
 declare split_if     [split del] split_if_asm     [split del] 
         option.split [split del] option.split_asm [split del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-change_claset (fn cs => cs delSWrapper "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+
 lemma FVar_lemma: 
 "\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
   G\<turnstile>statC\<preceq>\<^sub>C statDeclC;  
@@ -763,10 +762,8 @@
 declare split_paired_All [simp] split_paired_Ex [simp] 
 declare split_if     [split] split_if_asm     [split] 
         option.split [split] option.split_asm [split]
-ML_setup {*
-change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 
 
 lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; 
@@ -881,10 +878,9 @@
 declare split_paired_All [simp del] split_paired_Ex [simp del] 
 declare split_if     [split del] split_if_asm     [split del] 
         option.split [split del] option.split_asm [split del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-change_claset (fn cs => cs delSWrapper "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+
 lemma conforms_init_lvars: 
 "\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
   list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig);  
@@ -935,10 +931,8 @@
 declare split_paired_All [simp] split_paired_Ex [simp] 
 declare split_if     [split] split_if_asm     [split] 
         option.split [split] option.split_asm [split]
-ML_setup {*
-change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 
 
 subsection "accessibility"
diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/WellForm.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -1751,8 +1751,9 @@
 qed
  	      
 (* local lemma *)
-ML {* bind_thm("bexI'",permute_prems 0 1 bexI) *}
-ML {* bind_thm("ballE'",permute_prems 1 1 ballE) *}
+lemma bexI': "x \<in> A \<Longrightarrow> P x \<Longrightarrow> \<exists>x\<in>A. P x" by blast
+lemma ballE': "\<forall>x\<in>A. P x \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> Q" by blast
+
 lemma subint_widen_imethds: 
  "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J; jm \<in> imethds G J sig\<rbrakk> \<Longrightarrow>   
   \<exists> im \<in> imethds G I sig. is_static im = is_static jm \<and> 
@@ -2175,10 +2176,9 @@
 qed
 
 declare split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-change_claset (fn cs => cs delSWrapper "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+
 lemma dynamic_mheadsD:   
 "\<lbrakk>emh \<in> mheads G S statT sig;    
   G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh);
@@ -2306,10 +2306,8 @@
   qed
 qed
 declare split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 
 (* Tactical version *)
 (*
@@ -2452,10 +2450,9 @@
   
 
 declare split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-change_claset (fn cs => cs delSWrapper "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
+declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+
 lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
   dt=empty_dt \<longrightarrow> (case T of 
                      Inl T \<Rightarrow> is_type (prg E) T 
@@ -2478,10 +2475,8 @@
     )
 done
 declare split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 
 lemma ty_expr_is_type: 
 "\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
diff -r edd20fe274b5 -r 67bde7cfcf10 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/WellType.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -452,9 +452,7 @@
 declare not_None_eq [simp del] 
 declare split_if [split del] split_if_asm [split del]
 declare split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac")
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
 
 inductive_cases wt_elim_cases [cases set]:
 	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
@@ -490,9 +488,7 @@
 declare not_None_eq [simp] 
 declare split_if [split] split_if_asm [split]
 declare split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 
 lemma is_acc_class_is_accessible: 
   "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
@@ -606,25 +602,29 @@
 lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)"
   by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
 
-ML {*
-fun wt_fun name lhs =
-let
-  fun is_Inj (Const (inj,_) $ _) = true
-    | is_Inj _                   = false
-  fun pred (_ $ _ $ _ $ _ $ x) = is_Inj x
-in
-  cond_simproc name lhs pred (thm name)
-end
+simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
+    | _ => SOME (mk_meta_eq @{thm wt_expr_eq})) *}
+
+simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
+    | _ => SOME (mk_meta_eq @{thm wt_var_eq})) *}
 
-val wt_expr_proc  = wt_fun "wt_expr_eq"  "E,dt\<Turnstile>In1l t\<Colon>U";
-val wt_var_proc   = wt_fun "wt_var_eq"   "E,dt\<Turnstile>In2 t\<Colon>U";
-val wt_exprs_proc = wt_fun "wt_exprs_eq" "E,dt\<Turnstile>In3 t\<Colon>U";
-val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "E,dt\<Turnstile>In1r t\<Colon>U";
-*}
+simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
+    | _ => SOME (mk_meta_eq @{thm wt_exprs_eq})) *}
 
-ML {*
-Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
-*}
+simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = {*
+  fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
+    | _ => SOME (mk_meta_eq @{thm wt_stmt_eq})) *}
 
 lemma wt_elim_BinOp:
   "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;