--- a/src/HOL/Tools/Quotient/quotient_info.ML Sat Nov 05 10:59:11 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Sat Nov 05 12:01:21 2011 +0000
@@ -23,6 +23,7 @@
val transform_quotconsts: morphism -> quotconsts -> quotconsts
val lookup_quotconsts_global: theory -> term -> quotconsts option
val update_quotconsts: string -> quotconsts -> Context.generic -> Context.generic
+ val dest_quotconsts_global: theory -> quotconsts list
val dest_quotconsts: Proof.context -> quotconsts list
val print_quotconsts: Proof.context -> unit
@@ -156,6 +157,11 @@
fun dest_quotconsts ctxt =
flat (map snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
+fun dest_quotconsts_global thy =
+ flat (map snd (Symtab.dest (Quotconsts.get (Context.Theory thy))))
+
+
+
fun lookup_quotconsts_global thy t =
let
val (name, qty) = dest_Const t