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