src/Pure/codegen.ML
changeset 24688 a5754ca5c510
parent 24655 24b630fd008f
child 24707 dfeb98f84e93
     1.1 --- a/src/Pure/codegen.ML	Sun Sep 23 23:39:42 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Mon Sep 24 13:52:50 2007 +0200
     1.3 @@ -996,14 +996,14 @@
     1.4    in
     1.5      if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
     1.6      then
     1.7 -      (case try (fn state => interrupt_timeout (!auto_quickcheck_time_limit)
     1.8 +      (case try (fn state => TimeLimit.timeLimit (!auto_quickcheck_time_limit)
     1.9             (test_goal true (params, []) 1 assms) state) state of
    1.10           SOME (cex as SOME _) =>
    1.11             Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
    1.12               Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
    1.13         | _ => state)
    1.14      else state
    1.15 -  end handle Interrupt => state;
    1.16 +  end handle TimeLimit.TimeOut => state;
    1.17  
    1.18  val _ = Context.add_setup
    1.19    (Context.theory_map (Specification.add_theorem_hook test_goal'));