# HG changeset patch
# User blanchet
# Date 1376942376 -7200
# Node ID a58b3b8631c6caf288653b649123b62ea7e9c27f
# Parent  15fe0ca088b30e5b4e8bc0d1cd520587773409d0
keep long names to stay on the safe side

diff -r 15fe0ca088b3 -r a58b3b8631c6 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}