--- a/src/HOL/Bali/WellForm.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Bali/WellForm.thy Fri Apr 12 17:21:51 2013 +0200
@@ -2128,7 +2128,7 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
lemma dynamic_mheadsD:
"\<lbrakk>emh \<in> mheads G S statT sig;
@@ -2257,7 +2257,7 @@
qed
qed
declare split_paired_All [simp] split_paired_Ex [simp]
-declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
(* Tactical version *)
@@ -2402,7 +2402,7 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt 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
@@ -2426,7 +2426,7 @@
)
done
declare split_paired_All [simp] split_paired_Ex [simp]
-declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+setup {* map_theory_claset (fn ctxt => ctxt 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: