src/HOL/Bali/Basis.thy
changeset 17876 b9c92f384109
parent 17785 8d928051d6a7
child 18447 da548623916a
     1.1 --- a/src/HOL/Bali/Basis.thy	Mon Oct 17 23:10:10 2005 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Mon Oct 17 23:10:13 2005 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  
     1.5  declare split_if_asm  [split] option.split [split] option.split_asm [split]
     1.6  ML {*
     1.7 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
     1.8 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
     1.9  *}
    1.10  declare if_weak_cong [cong del] option.weak_case_cong [cong del]
    1.11  declare length_Suc_conv [iff];