# HG changeset patch
# User blanchet
# Date 1387529284 -3600
# Node ID 68c8f88af87ee9b3260d830e18fd15d2e4210e0a
# Parent  789fbbc092d2d2047aed87789244be9125c72b8d
compile

diff -r 789fbbc092d2 -r 68c8f88af87e src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Dec 19 21:49:30 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Dec 20 09:48:04 2013 +0100
@@ -24,6 +24,7 @@
 val ctxt = @{context}
 val stds = [(NONE, true)]
 val subst = []
+val tac_timeout = seconds 1.0
 val case_names = case_const_names ctxt stds
 val defs = all_defs_of thy subst
 val nondefs = all_nondefs_of ctxt subst
@@ -40,7 +41,7 @@
    stds = stds, wfs = [], user_axioms = NONE, debug = false,
    whacks = [], binary_ints = SOME false, destroy_constrs = true,
    specialize = false, star_linear_preds = false, total_consts = NONE,
-   needs = NONE, tac_timeout = NONE, evals = [], case_names = case_names,
+   needs = NONE, tac_timeout = tac_timeout, evals = [], case_names = case_names,
    def_tables = def_tables, nondef_table = nondef_table, nondefs = nondefs,
    simp_table = simp_table, psimp_table = psimp_table,
    choice_spec_table = choice_spec_table, intro_table = intro_table,
@@ -141,8 +142,8 @@
 ML_val {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
 
 ML {*
-val preproc_timeout = SOME (seconds 5.0)
-val mono_timeout = SOME (seconds 1.0)
+val preproc_timeout = seconds 5.0
+val mono_timeout = seconds 1.0
 
 fun all_unconcealed_theorems_of thy =
   let val facts = Global_Theory.facts_of thy in
@@ -172,8 +173,8 @@
       Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
     val free_Ts = fold Term.add_tfrees (op @ tsp) [] |> map TFree
     val (mono_free_Ts, nonmono_free_Ts) =
-      time_limit mono_timeout (List.partition is_type_actually_monotonic)
-                 free_Ts
+      TimeLimit.timeLimit mono_timeout
+          (List.partition is_type_actually_monotonic) free_Ts
   in
     if not (null mono_free_Ts) then "MONO"
     else if not (null nonmono_free_Ts) then "NONMONO"
@@ -192,7 +193,8 @@
         val t = th |> prop_of |> Type.legacy_freeze |> close_form
         val neg_t = Logic.mk_implies (t, @{prop False})
         val (nondef_ts, def_ts, _, _, _, _) =
-          time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
+          TimeLimit.timeLimit preproc_timeout (preprocess_formulas hol_ctxt [])
+                              neg_t
         val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
       in File.append path (res ^ "\n"); writeln res end
       handle TimeLimit.TimeOut => ()