src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 19 18:50:45 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 19 21:59:36 2013 +0200
@@ -566,7 +566,8 @@
 val pat_tvar_prefix = "_"
 val pat_var_prefix = "_"
 
-val massage_long_name = Long_Name.base_name
+(* try "Long_Name.base_name" for shorter names *)
+fun massage_long_name s = s
 
 val crude_str_of_sort =
   space_implode ":" o map massage_long_name o subtract (op =) @{sort type}