1.1 --- a/src/HOL/Bali/WellForm.thy	Mon Oct 17 23:10:10 2005 +0200
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Mon Oct 17 23:10:13 2005 +0200
     1.3 @@ -2178,8 +2178,8 @@
     1.4  
     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 -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  lemma dynamic_mheadsD:   
    1.13  "\<lbrakk>emh \<in> mheads G S statT sig;    
    1.14 @@ -2309,8 +2309,8 @@
    1.15  qed
    1.16  declare split_paired_All [simp] split_paired_Ex [simp]
    1.17  ML_setup {*
    1.18 -claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
    1.19 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    1.20 +change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
    1.21 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    1.22  *}
    1.23  
    1.24  (* Tactical version *)
    1.25 @@ -2455,8 +2455,8 @@
    1.26  
    1.27  declare split_paired_All [simp del] split_paired_Ex [simp del]
    1.28  ML_setup {*
    1.29 -simpset_ref() := simpset() delloop "split_all_tac";
    1.30 -claset_ref () := claset () delSWrapper "split_all_tac"
    1.31 +change_simpset (fn ss => ss delloop "split_all_tac");
    1.32 +change_claset (fn cs => cs delSWrapper "split_all_tac");
    1.33  *}
    1.34  lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
    1.35    dt=empty_dt \<longrightarrow> (case T of 
    1.36 @@ -2481,8 +2481,8 @@
    1.37  done
    1.38  declare split_paired_All [simp] split_paired_Ex [simp]
    1.39  ML_setup {*
    1.40 -claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
    1.41 -simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    1.42 +change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
    1.43 +change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    1.44  *}
    1.45  
    1.46  lemma ty_expr_is_type: