diff -r e2ac18492c68 -r baac4639ecef Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Sat Dec 19 22:09:57 2009 +0100
+++ b/Quot/quotient_def.ML	Sat Dec 19 22:21:51 2009 +0100
@@ -13,6 +13,9 @@
 structure Quotient_Def: QUOTIENT_DEF =
 struct
 
+open Quotient_Info;
+open Quotient_Type;
+
 (* wrapper for define *)
 fun define name mx attr rhs lthy =
 let
@@ -129,6 +132,6 @@
 
 end; (* structure *)
 
-open Quotient_Def;
 
 
+