changed first parameter of add_thydata and get_thydata
authorclasohm
Fri Apr 12 12:41:26 1996 +0200 (1996-04-12)
changeset 1657a7a6c3fb3cdd
parent 1656 cbba49da5139
child 1658 0eb69773354f
changed first parameter of add_thydata and get_thydata
src/HOL/HOL.ML
src/HOL/thy_data.ML
     1.1 --- a/src/HOL/HOL.ML	Thu Apr 11 13:41:22 1996 +0200
     1.2 +++ b/src/HOL/HOL.ML	Fri Apr 12 12:41:26 1996 +0200
     1.3 @@ -357,7 +357,7 @@
     1.4      fun put (SS_DATA ss) = simpset := ss;
     1.5  
     1.6      fun get () = SS_DATA (!simpset);
     1.7 -in add_thydata HOL.thy
     1.8 +in add_thydata "HOL"
     1.9       ("simpset", ThyMethods {merge = merge, put = put, get = get})
    1.10  end;
    1.11  
    1.12 @@ -371,7 +371,7 @@
    1.13      fun put (DT_DATA ds) = datatypes := ds;
    1.14  
    1.15      fun get () = DT_DATA (!datatypes);
    1.16 -in add_thydata HOL.thy
    1.17 +in add_thydata "HOL"
    1.18       ("datatypes", ThyMethods {merge = merge, put = put, get = get})
    1.19  end;
    1.20  
     2.1 --- a/src/HOL/thy_data.ML	Thu Apr 11 13:41:22 1996 +0200
     2.2 +++ b/src/HOL/thy_data.ML	Fri Apr 12 12:41:26 1996 +0200
     2.3 @@ -7,11 +7,11 @@
     2.4  *)
     2.5  
     2.6  fun simpset_of tname =
     2.7 -  case get_thydata (theory_of tname) "simpset" of
     2.8 +  case get_thydata tname "simpset" of
     2.9        None => empty_ss
    2.10      | Some (SS_DATA ss) => ss;
    2.11  
    2.12  fun datatypes_of tname =
    2.13 -  case get_thydata (theory_of tname) "datatypes" of
    2.14 +  case get_thydata tname "datatypes" of
    2.15        None => []
    2.16      | Some (DT_DATA ds) => ds;