src/HOL/Bali/WellType.thy
changeset 17876 b9c92f384109
parent 16417 9bc16273c2d4
child 21765 89275a3ed7be
     1.1 --- a/src/HOL/Bali/WellType.thy	Mon Oct 17 23:10:10 2005 +0200
     1.2 +++ b/src/HOL/Bali/WellType.thy	Mon Oct 17 23:10:13 2005 +0200
     1.3 @@ -469,7 +469,7 @@
     1.4  declare split_if [split del] split_if_asm [split del]
     1.5  declare split_paired_All [simp del] split_paired_Ex [simp del]
     1.6  ML_setup {*
     1.7 -simpset_ref() := simpset() delloop "split_all_tac"
     1.8 +change_simpset (fn ss => ss delloop "split_all_tac")
     1.9  *}
    1.10  
    1.11  inductive_cases wt_elim_cases [cases set]:
    1.12 @@ -507,7 +507,7 @@
    1.13  declare split_if [split] split_if_asm [split]
    1.14  declare split_paired_All [simp] split_paired_Ex [simp]
    1.15  ML_setup {*
    1.16 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    1.17 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    1.18  *}
    1.19  
    1.20  lemma is_acc_class_is_accessible: