--- a/QuotMain.thy	Sun Nov 29 23:59:37 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 12:26:08 2009 +0100
@@ -1217,6 +1217,9 @@
     end) lthy
 *}
 
+thm EQUIV_REFL
+thm equiv_trans2
+
 ML {*
 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
 fun lift_tac lthy rthm rel_eqv rty quot defs =

--- a/quotient_info.ML	Sun Nov 29 23:59:37 2009 +0100
+++ b/quotient_info.ML	Mon Nov 30 12:26:08 2009 +0100
@@ -11,6 +11,7 @@
   val quotdata_lookup: Proof.context -> string -> quotient_info option
   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
+  val quotdata_dest: theory -> quotient_info list
 
   type qconsts_info = {qconst: term, rconst: term}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
@@ -88,6 +89,9 @@
 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = 
       ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
 
+fun quotdata_dest thy =
+    map snd (Symtab.dest (QuotData.get thy))
+
 fun print_quotinfo ctxt =
 let
   fun prt_quot {qtyp, rtyp, rel, equiv_thm} =