--- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200
@@ -90,7 +90,8 @@
facts
|> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
|> take (the max_facts)
- val res as {outcome, ...} = run_prover ctxt params prover facts goal
+ val res as {outcome, ...} =
+ run_prover_for_mash ctxt params prover facts goal
val _ = if is_none outcome then ok := !ok + 1 else ()
in str_of_res heading facts res end
val iter_s = prove iter_ok iterN iter_facts