--- a/src/HOL/Bali/Basis.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Bali/Basis.thy Tue Feb 23 16:25:08 2016 +0100
@@ -11,7 +11,7 @@
ML \<open>fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i)\<close>
-declare split_if_asm [split] option.split [split] option.split_asm [split]
+declare if_split_asm [split] option.split [split] option.split_asm [split]
setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
declare if_weak_cong [cong del] option.case_cong_weak [cong del]
declare length_Suc_conv [iff]