--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 15:19:07 2014 +0100
@@ -100,27 +100,6 @@
|> Skip_Proof.make_thm thy
end
-fun tac_of_method ctxt (local_facts, global_facts) meth =
- Method.insert_tac local_facts THEN'
- (case meth of
- Metis_Method (type_enc_opt, lam_trans_opt) =>
- Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
- (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
- | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
- | Meson_Method => Meson.meson_tac ctxt global_facts
- | _ =>
- Method.insert_tac global_facts THEN'
- (case meth of
- Simp_Method => Simplifier.asm_full_simp_tac ctxt
- | Simp_Size_Method =>
- Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
- | Auto_Method => K (Clasimp.auto_tac ctxt)
- | Fastforce_Method => Clasimp.fast_force_tac ctxt
- | Force_Method => Clasimp.force_tac ctxt
- | Arith_Method => Arith_Data.arith_tac ctxt
- | Blast_Method => blast_tac ctxt
- | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
-
(* main function for preplaying Isar steps; may throw exceptions *)
fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
let
@@ -149,7 +128,7 @@
fun prove () =
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
- HEADGOAL (tac_of_method ctxt facts meth))
+ HEADGOAL (tac_of_proof_method ctxt facts meth))
handle ERROR msg => error ("Preplay error: " ^ msg)
val play_outcome = take_time timeout prove ()