src/HOL/Nitpick_Examples/Mono_Nits.thy
changeset 41805 a96684499e85
parent 41791 01d722707a36
child 41871 394eef237bd1
     1.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 21 18:02:14 2011 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 21 18:28:28 2011 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4    {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
     1.5     stds = stds, wfs = [], user_axioms = NONE, debug = false,
     1.6     whacks = [], binary_ints = SOME false, destroy_constrs = true,
     1.7 -   specialize = false, star_linear_preds = false,
     1.8 +   specialize = false, star_linear_preds = false, preconstrs = [],
     1.9     tac_timeout = NONE, evals = [], case_names = case_names,
    1.10     def_tables = def_tables, nondef_table = nondef_table,
    1.11     user_nondefs = user_nondefs, simp_table = simp_table,
    1.12 @@ -188,7 +188,7 @@
    1.13        let
    1.14          val t = th |> prop_of |> Type.legacy_freeze |> close_form
    1.15          val neg_t = Logic.mk_implies (t, @{prop False})
    1.16 -        val (nondef_ts, def_ts, _, _, _) =
    1.17 +        val (nondef_ts, def_ts, _, _, _, _) =
    1.18            time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
    1.19          val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
    1.20        in File.append path (res ^ "\n"); writeln res end