# HG changeset patch
# User blanchet
# Date 1360242332 -3600
# Node ID 4acc150a321ae835a5cd27ce7c3265400c8fe8ef
# Parent  98fb341d32e332af6fa28c91871733f4d9045f51
drop needless .0s

diff -r 98fb341d32e3 -r 4acc150a321a src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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