diff -r c1989de100b4 -r e2ac18492c68 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Sat Dec 19 22:04:34 2009 +0100
+++ b/Quot/quotient_tacs.ML	Sat Dec 19 22:09:57 2009 +0100
@@ -564,6 +564,7 @@
   error msg
 end
 
+open Quotient_Term;
  
 fun procedure_inst ctxt rtrm qtrm =
 let