Moved functions from file "thy_data.ML".
authorberghofe
Wed Aug 06 00:41:40 1997 +0200 (1997-08-06 ago)
changeset 36107e5300420b03
parent 3609 5756c98ebf1f
child 3611 3199f744cf4f
Moved functions from file "thy_data.ML".
src/FOL/cladata.ML
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/cladata.ML	Wed Aug 06 00:39:13 1997 +0200
     1.2 +++ b/src/FOL/cladata.ML	Wed Aug 06 00:41:40 1997 +0200
     1.3 @@ -61,6 +61,11 @@
     1.4  
     1.5  claset := FOL_cs;
     1.6  
     1.7 +fun claset_of tname =
     1.8 +  case get_thydata tname "claset" of
     1.9 +      None => empty_cs
    1.10 +    | Some (CS_DATA cs) => cs;
    1.11 +
    1.12  (*** Applying BlastFun to create Blast_tac ***)
    1.13  structure Blast_Data = 
    1.14    struct
     2.1 --- a/src/FOL/simpdata.ML	Wed Aug 06 00:39:13 1997 +0200
     2.2 +++ b/src/FOL/simpdata.ML	Wed Aug 06 00:41:40 1997 +0200
     2.3 @@ -247,9 +247,10 @@
     2.4       ("simpset", ThyMethods {merge = merge, put = put, get = get})
     2.5  end;
     2.6  
     2.7 -
     2.8 -add_thy_reader_file "thy_data.ML";
     2.9 -
    2.10 +fun simpset_of tname =
    2.11 +  case get_thydata tname "simpset" of
    2.12 +      None => empty_ss
    2.13 +    | Some (SS_DATA ss) => ss;
    2.14  
    2.15  
    2.16