diff -r 8bc7428745ad -r f32237ef18a6 quotient_info.ML
--- a/quotient_info.ML	Fri Nov 27 02:23:49 2009 +0100
+++ b/quotient_info.ML	Fri Nov 27 02:35:50 2009 +0100
@@ -12,11 +12,6 @@
   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
 
-  (*FIXME: obsolete *)
-  type qenv = (typ * typ) list
-  val mk_qenv: Proof.context -> qenv
-  val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option
-
   type qconsts_info = {qconst: term, rconst: term}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
   val qconsts_lookup: theory -> string -> qconsts_info option
@@ -116,22 +111,6 @@
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
 
 
-(* FIXME: obsolete: environments for quotient and raw types *)
-type qenv = (typ * typ) list
-
-fun mk_qenv ctxt =
-let
-  val thy = ProofContext.theory_of ctxt
-  val qinfo = (QuotData.get thy) |> Symtab.dest |> map snd
-in
-  map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) qinfo
-end
-
-fun lookup_qenv _ [] _ = NONE
-  | lookup_qenv eq ((qty, rty)::xs) qty' =
-      if eq (qty', qty) then SOME (qty, rty)
-      else lookup_qenv eq xs qty'
-
 (* information about quotient constants *)
 type qconsts_info = {qconst: term, rconst: term}