changeset 1657 | a7a6c3fb3cdd |
parent 1465 | 5d7a7e439cec |
child 1668 | 8ead1fe65aad |
--- a/src/HOL/thy_data.ML Thu Apr 11 13:41:22 1996 +0200 +++ b/src/HOL/thy_data.ML Fri Apr 12 12:41:26 1996 +0200 @@ -7,11 +7,11 @@ *) fun simpset_of tname = - case get_thydata (theory_of tname) "simpset" of + case get_thydata tname "simpset" of None => empty_ss | Some (SS_DATA ss) => ss; fun datatypes_of tname = - case get_thydata (theory_of tname) "datatypes" of + case get_thydata tname "datatypes" of None => [] | Some (DT_DATA ds) => ds;