--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:04 2012 +0200
@@ -53,7 +53,7 @@
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
n goal =
- (name,
+ (quote name,
(if verbose then
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
else
@@ -141,7 +141,7 @@
(outcome_code, state)
end
else
- (Async_Manager.launch das_tool birth_time death_time (desc ())
+ (Async_Manager.launch SledgehammerN birth_time death_time (desc ())
((fn (outcome_code, message) =>
(verbose orelse outcome_code = someN,
message ())) o go);