# HG changeset patch
# User wenzelm
# Date 1258310656 -3600
# Node ID b5f36fa5a7b4b482cf401d8f21637cf14a55e27c
# Parent  7d6793ce0a2653ba15462b5f994d7403ebe01c24
provide actual Nitpick_HOL.extended_context;

diff -r 7d6793ce0a26 -r b5f36fa5a7b4 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sun Nov 15 15:14:28 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sun Nov 15 19:44:16 2009 +0100
@@ -16,7 +16,7 @@
 
 val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1
 val def_table = Nitpick_HOL.const_def_table @{context} defs
-val ext_ctxt =
+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,
@@ -26,7 +26,8 @@
    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 []}
+   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 =