# HG changeset patch
# User wenzelm
# Date 1320525416 -3600
# Node ID 8b1604119bc0f22fd681229e5b16ea368b5a0c21
# Parent  257d0b179f0d1defd5fc6b95243a8e7701c95910# Parent  7fb63b469cd290eaf604c08fe364235cdb83ca29
merged

diff -r 7fb63b469cd2 -r 8b1604119bc0 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Sat Nov 05 20:40:30 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Sat Nov 05 21:36:56 2011 +0100
@@ -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
diff -r 7fb63b469cd2 -r 8b1604119bc0 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Nov 05 20:40:30 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Nov 05 21:36:56 2011 +0100
@@ -521,7 +521,8 @@
 *)
 fun clean_tac lthy =
   let
-    val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts lthy)
+    val thy =  Proof_Context.theory_of lthy
+    val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts_global thy)
     val prs = Quotient_Info.prs_rules lthy
     val ids = Quotient_Info.id_simps lthy
     val thms =