# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259839339 -3600
# Node ID b663bc007d00855de4b29f2eb1b09b856c1f02e9
# Parent  8f1bf5266ebc89dc7dca79f4096fde57e0acdce4
Added qoutient_consts dest for getting all the constant definitions in the cleaning step.

diff -r 8f1bf5266ebc -r b663bc007d00 quotient_info.ML
--- 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