adapted to new implicit simpset;
authorwenzelm
Mon Nov 03 12:28:01 1997 +0100 (1997-11-03 ago)
changeset 40949e501199ec01
parent 4093 5e8f3d57dee7
child 4095 6fd0f439e50e
adapted to new implicit simpset;
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Mon Nov 03 12:26:58 1997 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Mon Nov 03 12:28:01 1997 +0100
     1.3 @@ -197,8 +197,8 @@
     1.4  fun ss delcongs congs =
     1.5          ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection]));
     1.6  
     1.7 -fun Addcongs congs = (simpset := !simpset addcongs congs);
     1.8 -fun Delcongs congs = (simpset := !simpset delcongs congs);
     1.9 +fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    1.10 +fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    1.11  
    1.12  val IFOL_simps =
    1.13     [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
    1.14 @@ -235,29 +235,7 @@
    1.15  (*classical simprules too*)
    1.16  val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps);
    1.17  
    1.18 -
    1.19 -
    1.20 -(*** Install simpsets and datatypes in theory structure ***)
    1.21 -
    1.22 -simpset := FOL_ss;
    1.23 -
    1.24 -exception SS_DATA of simpset;
    1.25 -
    1.26 -let fun merge [] = SS_DATA empty_ss
    1.27 -      | merge ss = let val ss = map (fn SS_DATA x => x) ss;
    1.28 -                   in SS_DATA (foldl merge_ss (hd ss, tl ss)) end;
    1.29 -
    1.30 -    fun put (SS_DATA ss) = simpset := ss;
    1.31 -
    1.32 -    fun get () = SS_DATA (!simpset);
    1.33 -in add_thydata "FOL"
    1.34 -     ("simpset", ThyMethods {merge = merge, put = put, get = get})
    1.35 -end;
    1.36 -
    1.37 -fun simpset_of tname =
    1.38 -  case get_thydata tname "simpset" of
    1.39 -      None => empty_ss
    1.40 -    | Some (SS_DATA ss) => ss;
    1.41 +simpset_ref() := FOL_ss;
    1.42  
    1.43  
    1.44  
    1.45 @@ -294,7 +272,7 @@
    1.46  fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
    1.47  fun cs addss  ss = cs addbefore                        asm_full_simp_tac ss;
    1.48  
    1.49 -fun Addss ss = (claset := !claset addss ss);
    1.50 +fun Addss ss = (claset_ref() := claset() addss ss);
    1.51  
    1.52  (*Designed to be idempotent, except if best_tac instantiates variables
    1.53    in some of the subgoals*)
    1.54 @@ -327,6 +305,6 @@
    1.55  	       prune_params_tac] 
    1.56      end;
    1.57  
    1.58 -fun Auto_tac () = auto_tac (!claset, !simpset);
    1.59 +fun Auto_tac () = auto_tac (claset(), simpset());
    1.60  
    1.61  fun auto () = by (Auto_tac ());