--- a/src/HOL/Bali/WellType.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/Bali/WellType.thy Thu May 16 17:39:38 2013 +0200
@@ -494,7 +494,7 @@
declare not_None_eq [simp]
declare split_if [split] split_if_asm [split]
declare split_paired_All [simp] split_paired_Ex [simp]
-setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
+setup {* map_theory_simpset (fn ctxt => ctxt 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"