# 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 =