--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Dec 17 22:06:28 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Dec 17 22:06:28 2012 +0100
@@ -358,6 +358,8 @@
NONE
| _ => NONE
+val instantiate_induct_timeout = seconds 0.01
+
fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
let
fun varify_noninducts (t as Free (s, T)) =
@@ -381,7 +383,8 @@
SOME (p_name, ind_T) =>
let val thy = Proof_Context.theory_of ctxt in
stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
- |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
+ |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
+ (instantiate_induct_rule ctxt stmt p_name ax)))
end
| NONE => [ax]