# HG changeset patch
# User blanchet
# Date 1267006078 -3600
# Node ID 34819133c75e31f42c45c88d2c1d7ae19d1a76ab
# Parent  38848da259c0027ac247f22526d5e74bb8170df6
make example compile

diff -r 38848da259c0 -r 34819133c75e src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Feb 24 09:59:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Feb 24 11:07:58 2010 +0100
@@ -14,8 +14,9 @@
 ML {*
 exception FAIL
 
-val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1
-val def_table = Nitpick_HOL.const_def_table @{context} defs
+val subst = []
+val defs = Nitpick_HOL.all_axioms_of @{theory} subst |> #1
+val def_table = Nitpick_HOL.const_def_table @{context} subst defs
 val hol_ctxt : Nitpick_HOL.hol_context =
   {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
    stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
diff -r 38848da259c0 -r 34819133c75e src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Wed Feb 24 09:59:54 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Wed Feb 24 11:07:58 2010 +0100
@@ -2,6 +2,7 @@
 
   * Added and implemented "binary_ints" and "bits" options
   * Added "std" option and implemented support for nonstandard models
+  * Added support for quotient types
   * Added support for local definitions
   * Optimized "Multiset.multiset"
   * Fixed soundness bugs related to "destroy_constrs" optimization and record