--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:36 2011 +0200
@@ -416,8 +416,9 @@
val full_tac = Method.insert_tac facts i THEN tac ctxt i
in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
-fun tac_for_reconstructor Metis = Metis_Tactics.old_metisH_tac
- | tac_for_reconstructor MetisFT = Metis_Tactics.old_metisFT_tac
+fun tac_for_reconstructor Metis =
+ Metis_Tactics.new_metis_tac [Metis_Tactics.default_unsound_type_sys]
+ | tac_for_reconstructor MetisFT = Metis_Tactics.new_metisFT_tac
| tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
fun timed_reconstructor reconstructor debug timeout ths =