--- a/src/HOL/Bali/Eval.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/Bali/Eval.thy Thu May 16 17:39:38 2013 +0200
@@ -818,7 +818,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]
-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))) *}
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]