# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265302703 -3600
# Node ID 0391abfc624676ccbe026f4c7363ab84d90d1d23
# Parent  b93b631570ca773171c683bfb245eab5fb58b923
Quotdata_dest needed for lifting theorem translation.

diff -r b93b631570ca -r 0391abfc6246 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Feb 04 17:39:04 2010 +0100
+++ b/Quot/quotient_info.ML	Thu Feb 04 17:58:23 2010 +0100
@@ -23,6 +23,7 @@
   val quotdata_lookup: theory -> string -> 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 quotdata_dest: Proof.context -> quotdata_info list
   val print_quotinfo: Proof.context -> unit
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
@@ -166,6 +167,9 @@
 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_dest lthy =
+  map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy)))
+
 fun print_quotinfo ctxt =
 let
   fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =