--- a/quotient_def.ML	Wed Nov 04 12:07:22 2009 +0100
+++ b/quotient_def.ML	Wed Nov 04 12:19:04 2009 +0100
@@ -24,11 +24,6 @@
   ((rhs, thm), lthy')
 end
 
-fun lookup_qenv qenv qty =
-  (case (AList.lookup (op=) qenv qty) of
-    SOME rty => SOME (qty, rty)
-  | NONE => NONE)
-
 
 (* calculates the aggregate abs and rep functions for a given type; 
    repF is for constants' arguments; absF is for constants;
@@ -81,7 +76,7 @@
 
 in
   if (AList.defined (op=) qenv ty)
-  then (get_const flag (the (lookup_qenv qenv ty)))
+  then (get_const flag (the (Quotient_Info.lookup_qenv (op=) qenv ty)))
   else (case ty of
           TFree _ => (mk_identity ty, (ty, ty))
         | Type (_, []) => (mk_identity ty, (ty, ty))