src/HOL/Bali/Basis.thy

--- a/src/HOL/Bali/Basis.thy	Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Bali/Basis.thy	Mon Oct 17 23:10:13 2005 +0200
@@ -25,7 +25,7 @@
 
 declare split_if_asm  [split] option.split [split] option.split_asm [split]
 ML {*
-simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
 *}
 declare if_weak_cong [cong del] option.weak_case_cong [cong del]
 declare length_Suc_conv [iff];