src/HOL/cladata.ML
changeset 4085 6e2d41a5ea43
parent 4059 59c1422c9da5
child 4179 cc4b6791d5dc
     1.1 --- a/src/HOL/cladata.ML	Mon Nov 03 12:07:13 1997 +0100
     1.2 +++ b/src/HOL/cladata.ML	Mon Nov 03 12:09:20 1997 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Tobias Nipkow
     1.5      Copyright   1996  University of Cambridge
     1.6  
     1.7 -Setting up the classical reasoner 
     1.8 +Setting up the classical reasoner.
     1.9  *)
    1.10  
    1.11  
    1.12 @@ -46,25 +46,7 @@
    1.13  val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
    1.14                       addSEs [exE] addEs [allE];
    1.15  
    1.16 -exception CS_DATA of claset;
    1.17 -
    1.18 -let fun merge [] = CS_DATA empty_cs
    1.19 -      | merge cs = let val cs = map (fn CS_DATA x => x) cs;
    1.20 -                   in CS_DATA (foldl merge_cs (hd cs, tl cs)) end;
    1.21 -
    1.22 -    fun put (CS_DATA cs) = claset := cs;
    1.23 -
    1.24 -    fun get () = CS_DATA (!claset);
    1.25 -in add_thydata "HOL"
    1.26 -     ("claset", ThyMethods {merge = merge, put = put, get = get})
    1.27 -end;
    1.28 -
    1.29 -fun claset_of tname =
    1.30 -  case get_thydata tname "claset" of
    1.31 -      None => empty_cs
    1.32 -    | Some (CS_DATA cs) => cs;
    1.33 -
    1.34 -claset := HOL_cs;
    1.35 +claset_ref() := HOL_cs;
    1.36  
    1.37  (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
    1.38  qed_goal "alt_ex1E" thy