--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Feb 07 14:05:32 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Feb 07 14:05:32 2013 +0100
@@ -210,7 +210,7 @@
fun encode_feature (name, weight) =
encode_str name ^
- (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
+ (if Real.== (weight, 1.0) then "" else "=" ^ smart_string_of_real weight)
val encode_features = map encode_feature #> space_implode " "
@@ -330,7 +330,7 @@
local
-val version = "*** MaSh version 20130113a ***"
+val version = "*** MaSh version 20130207a ***"
exception Too_New of unit