--- 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,
--- 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