# HG changeset patch
# User blanchet
# Date 1471170369 -7200
# Node ID af310e622d643fd9208b1720c62398ee0cfa2f06
# Parent  9ad6a63cc8bdc95b3cd36e1a03a69f9b003b50bb
tuned MaSh's metacharacters to avoid needless decoding

diff -r 9ad6a63cc8bd -r af310e622d64 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Aug 14 12:26:09 2016 +0200
@@ -518,7 +518,7 @@
 
 fun meta_char c =
   if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse
-     c = #"," then
+     c = #"," orelse c = #"'" then
     String.str c
   else
     (* fixed width, in case more digits follow *)
@@ -639,7 +639,7 @@
 
 local
 
-val version = "*** MaSh version 20151004 ***"
+val version = "*** MaSh version 20160805 ***"
 
 exception FILE_VERSION_TOO_NEW of unit
 
@@ -850,7 +850,7 @@
 (* 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}
+val crude_str_of_sort = space_implode "," o map massage_long_name o subtract (op =) @{sort type}
 
 fun crude_str_of_typ (Type (s, [])) = massage_long_name s
   | crude_str_of_typ (Type (s, Ts)) = massage_long_name s ^ implode (map crude_str_of_typ Ts)