changeset 51990 | cc66addbba6d |
parent 51187 | c344cf148e8f |
child 51998 | f732a674db1b |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue May 14 20:32:10 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue May 14 20:46:09 2013 +0200 @@ -219,7 +219,7 @@ fun encode_feature (name, weight) = encode_str name ^ - (if Real.== (weight, 1.0) then "" else "=" ^ smart_string_of_real weight) + (if Real.== (weight, 1.0) then "" else "=" ^ Markup.print_real weight) val encode_features = map encode_feature #> space_implode " "