--- a/src/HOL/Tools/Quotient/quotient_type.ML Wed Nov 30 10:07:32 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Wed Nov 30 11:36:46 2011 +0100
@@ -214,23 +214,8 @@
end
-
(*** interface and syntax setup ***)
-
-(* the ML-interface takes a list of 5-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
-
- 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 *)