more use of global operations (see 98ec8b51af9c)

--- 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

--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Nov 05 10:59:11 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Nov 05 12:01:21 2011 +0000
@@ -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 =