--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Dec 14 16:48:49 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Dec 17 15:22:11 2009 +0100
@@ -18,16 +18,16 @@
val def_table = Nitpick_HOL.const_def_table @{context} defs
val ext_ctxt : Nitpick_HOL.extended_context =
{thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
- user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false,
- specialize = false, skolemize = false, star_linear_preds = false,
- uncurry = false, fast_descrs = false, tac_timeout = NONE, evals = [],
- case_names = [], def_table = def_table, nondef_table = Symtab.empty,
- user_nondefs = [], simp_table = Unsynchronized.ref Symtab.empty,
- psimp_table = Symtab.empty, intro_table = Symtab.empty,
- ground_thm_table = Inttab.empty, ersatz_table = [],
- skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
- unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
- constr_cache = Unsynchronized.ref []}
+ user_axioms = NONE, debug = false, wfs = [], binary_ints = SOME false,
+ destroy_constrs = false, specialize = false, skolemize = false,
+ star_linear_preds = false, uncurry = false, fast_descrs = false,
+ tac_timeout = NONE, evals = [], case_names = [], def_table = def_table,
+ nondef_table = Symtab.empty, user_nondefs = [],
+ simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
+ intro_table = Symtab.empty, ground_thm_table = Inttab.empty,
+ ersatz_table = [], skolems = Unsynchronized.ref [],
+ special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
+ wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
(* term -> bool *)
val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a} [] []
fun is_const t =