# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257333544 -3600
# Node ID 0e89332f7625c19318f56b4ab51c442e4574c559
# Parent  b2fd070c88338cbd664ff6919cc90556a9831adf
more tuning

diff -r b2fd070c8833 -r 0e89332f7625 quotient_def.ML
--- 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))