diff -r e2ac18492c68 -r baac4639ecef Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Sat Dec 19 22:09:57 2009 +0100
+++ b/Quot/quotient_term.ML	Sat Dec 19 22:21:51 2009 +0100
@@ -7,6 +7,10 @@
 structure Quotient_Term: QUOTIENT_TERM =
 struct
 
+open Quotient_Info;
+open Quotient_Type;
+open Quotient_Def;
+
 (*
 Regularizing an rtrm means: