src/FOL/simpdata.ML
changeset 3610 7e5300420b03
parent 3566 c9c351374651
child 3835 9a5a4e123859
     1.1 --- a/src/FOL/simpdata.ML	Wed Aug 06 00:39:13 1997 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Wed Aug 06 00:41:40 1997 +0200
     1.3 @@ -247,9 +247,10 @@
     1.4       ("simpset", ThyMethods {merge = merge, put = put, get = get})
     1.5  end;
     1.6  
     1.7 -
     1.8 -add_thy_reader_file "thy_data.ML";
     1.9 -
    1.10 +fun simpset_of tname =
    1.11 +  case get_thydata tname "simpset" of
    1.12 +      None => empty_ss
    1.13 +    | Some (SS_DATA ss) => ss;
    1.14  
    1.15  
    1.16