--- a/src/HOL/Bali/Evaln.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/Bali/Evaln.thy Thu May 16 17:39:38 2013 +0200
@@ -238,7 +238,7 @@
option.split [split] option.split_asm [split]
not_None_eq [simp]
split_paired_All [simp] split_paired_Ex [simp]
-declaration {* K (Simplifier.map_ss (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>)