--- a/quotient_info.ML	Thu Dec 03 12:17:23 2009 +0100
+++ b/quotient_info.ML	Thu Dec 03 12:22:19 2009 +0100
@@ -17,7 +17,8 @@
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
   val qconsts_lookup: theory -> string -> qconsts_info option
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
-  val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic 
+  val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
+  val qconsts_dest: theory -> qconsts_info list
   val print_qconstinfo: Proof.context -> unit
 
   val rsp_rules_get: Proof.context -> thm list  
@@ -136,6 +137,9 @@
 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I
 
+fun qconsts_dest thy =
+    map snd (Symtab.dest (QConstsData.get thy))
+
 (* We don't print the definition *)
 fun print_qconstinfo ctxt =
 let