author | blanchet |
Wed, 11 Jul 2012 11:28:27 +0200 | |
changeset 48242 | 713e32be9845 |
parent 48241 | 688f1172d523 |
child 48244 | b88c3e0b752e |
--- a/src/HOL/TPTP/mash_export.ML Wed Jul 11 11:28:10 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 11 11:28:27 2012 +0200 @@ -179,6 +179,7 @@ val max_depth = 1 +(* TODO: Generate type classes for types? *) fun features_of thy (status, th) = let val t = Thm.prop_of th in thy_name_of (thy_name_of_thm th) ::