Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 50401 8e5d7ef3da76
parent 50398 78c7b52dbadb
child 50412 e83ab94e3e6e 
--- 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 =
isabelle