# HG changeset patch
# User blanchet
# Date 1354789510 -3600
# Node ID ad0ac9112d2c18d754c5f6cc71acede82b34fa39
# Parent  a5b666e0c3c261eeb44a032fd0449b52f29d8c3d
simplify code now that "mash.py" supports weights

diff -r a5b666e0c3c2 -r ad0ac9112d2c src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
@@ -180,18 +180,9 @@
 val unescape_metas =
   space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
 
-val supports_weights = false
-
 fun encode_feature (name, weight) =
-  let val s = escape_meta name in
-    if Real.== (weight, 1.0) then
-      s
-    else if supports_weights then
-      s ^ "=" ^ Real.toString weight
-    else
-      map (prefix (s ^ ".") o string_of_int) (1 upto Real.ceil weight)
-      |> space_implode " "
-  end
+  escape_meta name ^
+  (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
 
 val encode_features = map encode_feature #> space_implode " "