src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 56254 a2dd9200854d
parent 55642 63beb38e9258
child 56303 4cc3f4db3447
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -577,7 +577,7 @@
     1.4  val pat_var_prefix = "_"
     1.5  
     1.6  (* try "Long_Name.base_name" for shorter names *)
     1.7 -fun massage_long_name s = if s = hd HOLogic.typeS then "T" else s
     1.8 +fun massage_long_name s = if s = @{class type} then "T" else s
     1.9  
    1.10  val crude_str_of_sort =
    1.11    space_implode ":" o map massage_long_name o subtract (op =) @{sort type}