--- a/Quot/quotient_info.ML	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/quotient_info.ML	Wed Dec 09 15:57:47 2009 +0100
@@ -17,8 +17,8 @@
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
-  val qconsts_lookup: theory -> string -> qconsts_info
-  val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
+  val qconsts_lookup: theory -> term -> qconsts_info
+  val qconsts_update_thy: string -> qconsts_info -> theory -> theory
   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
   val qconsts_dest: theory -> qconsts_info list
   val print_qconstinfo: Proof.context -> unit
@@ -145,16 +145,27 @@
      rconst = Morphism.term phi rconst,
      def = Morphism.thm phi def}
 
-fun qconsts_lookup thy str = 
-  case Symtab.lookup (QConstsData.get thy) str of
-    SOME info => info
-  | NONE => raise NotFound
-
-fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
-fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I
+fun qconsts_update_thy id qcinfo = QConstsData.map (Symtab.update (id, qcinfo))
+fun qconsts_update_gen id qcinfo = Context.mapping (qconsts_update_thy id qcinfo) I
 
 fun qconsts_dest thy =
-    map snd (Symtab.dest (QConstsData.get thy))
+  map snd (Symtab.dest (QConstsData.get thy))
+
+fun qconsts_lookup thy t =
+  let
+    val smt = Symtab.dest (QConstsData.get thy);
+    val (name, qty) = dest_Const t
+    fun matches (_, x) =
+      let
+        val (name', qty') = dest_Const (#qconst x);
+      in
+        name = name' andalso Sign.typ_instance thy (qty, qty')
+      end
+  in
+    case (find_first matches smt) of
+      SOME (_, x) => x
+    | _ => raise NotFound
+  end
 
 (* We don't print the definition *)
 fun print_qconstinfo ctxt =