Quot/quotient_typ.ML
changeset 762 baac4639ecef
parent 760 c1989de100b4
child 766 df053507edba
--- 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
+