--- 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