# HG changeset patch
# User kuncar
# Date 1322649406 -3600
# Node ID e903a390370cbc59e60e612ab6679b221917d4a7
# Parent  4c25ba9f3c23a1daac4ed4e5c5bc21a99f36a8f0
removed outdated comment

diff -r 4c25ba9f3c23 -r e903a390370c src/HOL/Tools/Quotient/quotient_type.ML
--- 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 *)