--- a/src/HOL/Quickcheck_Exhaustive.thy Wed Nov 30 18:07:14 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Wed Nov 30 19:18:17 2011 +0100
@@ -537,7 +537,9 @@
code_const catch_match'
(Quickcheck "(_) handle Match => _")
-consts unknown :: "'a" ("?")
+axiomatization unknown :: 'a
+
+notation (output) unknown ("?")
use "Tools/Quickcheck/exhaustive_generators.ML"
@@ -547,7 +549,7 @@
hide_fact orelse_def catch_match_def
no_notation orelse (infixr "orelse" 55)
-hide_const (open) orelse catch_match mk_map_term check_all_n_lists
+hide_const (open) orelse catch_match catch_match' unknown mk_map_term check_all_n_lists
hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
--- a/src/HOL/Tools/Quotient/quotient_type.ML Wed Nov 30 18:07:14 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Wed Nov 30 19:18:17 2011 +0100
@@ -216,6 +216,20 @@
(*** interface and syntax setup ***)
+(* the ML-interface takes a list of tuples consisting of:
+
+ - the name of the quotient type
+ - its free type variables (first argument)
+ - its mixfix annotation
+ - the type to be quotient
+ - the partial flag (a boolean)
+ - the relation according to which the type is quotient
+ - optional names of morphisms (rep/abs)
+
+ it opens a proof-state in which one has to show that the
+ relations are equivalence relations
+*)
+
fun quotient_type quot_list lthy =
let
(* sanity check *)