diff -r 3764566c1151 -r 4d58c02289ca quotient_info.ML
--- a/quotient_info.ML	Tue Nov 03 16:17:19 2009 +0100
+++ b/quotient_info.ML	Tue Nov 03 16:51:33 2009 +0100
@@ -11,11 +11,16 @@
   val quotdata_lookup: Proof.context -> quotient_info list
   val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context
+
+  type qenv = (typ * typ) list
+  val mk_qenv: Proof.context -> qenv
+  val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option
 end;
 
 structure Quotient_Info: QUOTIENT_INFO =
 struct
 
+
 (* data containers *)
 (*******************)
 
@@ -102,6 +107,22 @@
   OuterSyntax.improper_command "print_quotients" "print out all quotients" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of)))
 
+
+(* environments of quotient and raw types *)
+type qenv = (typ * typ) list
+
+fun mk_qenv ctxt =
+let
+  val qinfo = quotdata_lookup ctxt
+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'
+
 end; (* structure *)
 
 open Quotient_Info
\ No newline at end of file