--- a/src/HOL/Bali/Basis.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/Bali/Basis.thy Thu May 16 17:39:38 2013 +0200
@@ -12,7 +12,7 @@
ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *}
declare split_if_asm [split] option.split [split] option.split_asm [split]
-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)) *}
declare if_weak_cong [cong del] option.weak_case_cong [cong del]
declare length_Suc_conv [iff]