diff -r e2ac18492c68 -r baac4639ecef Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Sat Dec 19 22:09:57 2009 +0100
+++ b/Quot/quotient_typ.ML	Sat Dec 19 22:21:51 2009 +0100
@@ -1,4 +1,4 @@
-signature QUOTIENT =
+signature QUOTIENT_TYPE =
 sig
   exception LIFT_MATCH of string
 
@@ -7,9 +7,11 @@
 
 end;
 
-structure Quotient: QUOTIENT =
+structure Quotient_Type: QUOTIENT_TYPE =
 struct
 
+open Quotient_Info;
+
 exception LIFT_MATCH of string
 
 (* wrappers for define, note, Attrib.internal and theorem_i *)
@@ -223,4 +225,4 @@
 
 end; (* structure *)
 
-open Quotient
+