add a timeout in induction rule instantiation
authorblanchet
Mon Dec 17 22:06:28 2012 +0100 (2012-12-17)
changeset 50586e31ee2076db1
parent 50585 306c7b807e13
child 50587 bd6582be1562
add a timeout in induction rule instantiation
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Dec 17 22:06:28 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Dec 17 22:06:28 2012 +0100
     1.3 @@ -358,6 +358,8 @@
     1.4        NONE
     1.5    | _ => NONE
     1.6  
     1.7 +val instantiate_induct_timeout = seconds 0.01
     1.8 +
     1.9  fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
    1.10    let
    1.11      fun varify_noninducts (t as Free (s, T)) =
    1.12 @@ -381,7 +383,8 @@
    1.13      SOME (p_name, ind_T) =>
    1.14      let val thy = Proof_Context.theory_of ctxt in
    1.15        stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
    1.16 -              |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
    1.17 +              |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
    1.18 +                     (instantiate_induct_rule ctxt stmt p_name ax)))
    1.19      end
    1.20    | NONE => [ax]
    1.21