# HG changeset patch
# User blanchet
# Date 1355778388 -3600
# Node ID e31ee2076db1b96214932435ef96a52589c942a3
# Parent  306c7b807e136d3c59ccbe45bbf807eae2945ea8
add a timeout in induction rule instantiation

diff -r 306c7b807e13 -r e31ee2076db1 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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]