# HG changeset patch
# User blanchet
# Date 1354805657 -3600
# Node ID 8e5d7ef3da7610d14cae3d1aca43f8ec892b144d
# Parent  fe9223fdd0603ffc7974c12e2dd819aee560d710
parse more liberal MaSh suggestion syntax (for the eval driver)

diff -r fe9223fdd060 -r 8e5d7ef3da76 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:42:23 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 15:54:17 2012 +0100
@@ -199,7 +199,8 @@
 fun extract_suggestion sugg =
   case space_explode "=" sugg of
     [name, weight] =>
-    SOME (unescape_meta name, Real.fromString weight |> the_default 0.0)
+    SOME (unescape_meta name, Real.fromString weight |> the_default 1.0)
+  | [name] => SOME (unescape_meta name, 1.0)
   | _ => NONE
 
 fun extract_query line =