changeset 49257 | 713e32be9845 |
parent 49255 | 6a8d18798161 |
child 49260 | 854a47677335 |
1.1 --- a/src/HOL/TPTP/mash_export.ML Wed Jul 11 11:28:10 2012 +0200 1.2 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 11 11:28:27 2012 +0200 1.3 @@ -179,6 +179,7 @@ 1.4 1.5 val max_depth = 1 1.6 1.7 +(* TODO: Generate type classes for types? *) 1.8 fun features_of thy (status, th) = 1.9 let val t = Thm.prop_of th in 1.10 thy_name_of (thy_name_of_thm th) ::