diff -r c4fa87dd0208 -r c2501b2b262a Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Mon Jan 11 11:51:19 2010 +0100
+++ b/Quot/quotient_info.ML	Mon Jan 11 15:13:09 2010 +0100
@@ -12,7 +12,6 @@
   type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
   val transform_quotdata: morphism -> quotdata_info -> quotdata_info
   val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
-  val quotdata_lookup_type: theory -> typ -> quotdata_info   (* raises NotFound *)
   val quotdata_update_thy: string -> quotdata_info -> theory -> theory
   val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
   val print_quotinfo: Proof.context -> unit
@@ -159,16 +158,6 @@
 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
 
-fun quotdata_lookup_type thy qty =
-  let
-    val smt = Symtab.dest (QuotData.get thy);
-    fun matches (_, x) = Sign.typ_instance thy (qty, (#qtyp x))
-  in
-    case (find_first matches smt) of
-      SOME (_, x) => x
-    | _ => raise NotFound
-  end
-
 fun print_quotinfo ctxt =
 let
   fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =