src/HOL/TPTP/mash_export.ML
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) ::