src/HOL/Bali/AxSem.thy
changeset 17876 b9c92f384109
parent 16417 9bc16273c2d4
child 19685 4477003648cc
     1.1 --- a/src/HOL/Bali/AxSem.thy	Mon Oct 17 23:10:10 2005 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Mon Oct 17 23:10:13 2005 +0200
     1.3 @@ -483,8 +483,8 @@
     1.4  declare split_if     [split del] split_if_asm     [split del] 
     1.5          option.split [split del] option.split_asm [split del]
     1.6  ML_setup {*
     1.7 -simpset_ref() := simpset() delloop "split_all_tac";
     1.8 -claset_ref () := claset () delSWrapper "split_all_tac"
     1.9 +change_simpset (fn ss => ss delloop "split_all_tac");
    1.10 +change_claset (fn cs => cs delSWrapper "split_all_tac");
    1.11  *}
    1.12  
    1.13  inductive "ax_derivs G" intros