src/HOL/Tools/Nitpick/nitpick.ML
changeset 41007 75275c796b46
parent 41001 11715564e2ad
child 41048 d5ebe94248ad
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -270,7 +270,7 @@
     1.4      val intro_table = inductive_intro_table ctxt subst def_table
     1.5      val ground_thm_table = ground_theorem_table thy
     1.6      val ersatz_table = ersatz_table ctxt
     1.7 -    val (hol_ctxt as {wf_cache, ...}) =
     1.8 +    val hol_ctxt as {wf_cache, ...} =
     1.9        {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
    1.10         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    1.11         whacks = whacks, binary_ints = binary_ints,