--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Aug 14 12:26:09 2016 +0200
@@ -289,11 +289,13 @@
"Filtering " ^ string_of_int (length all_facts) ^ " facts (MaSh algorithm: " ^
str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
in
+timeit (fn () =>
all_facts
|> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
|> tap (fn factss => if verbose then print (string_of_factss factss) else ())
|> spy ? tap (fn factss => spying spy (fn () =>
(state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
+) (*###*)
end
fun launch_provers () =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Aug 14 12:26:09 2016 +0200
@@ -533,10 +533,13 @@
| unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
val encode_str = String.translate meta_char
-val decode_str = String.explode #> unmeta_chars []
+val encode_strs = map encode_str #> space_implode " "
-val encode_strs = map encode_str #> space_implode " "
-val decode_strs = space_explode " " #> map decode_str
+fun decode_str s =
+ if String.isSubstring "%" s then unmeta_chars [] (String.explode s) else s;
+
+fun decode_strs s =
+ space_explode " " s |> String.isSubstring "%" s ? map decode_str;
datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop