# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263462663 -3600
# Node ID 4163fe3dbf8c976d75bf0bd9076b8654eac55987
# Parent  2a19e0a37131edaf5e8da88e30e129cb28a11a1b
produce defs with lthy, like prs and ids

diff -r 2a19e0a37131 -r 4163fe3dbf8c Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Jan 14 10:47:19 2010 +0100
+++ b/Quot/quotient_info.ML	Thu Jan 14 10:51:03 2010 +0100
@@ -21,7 +21,7 @@
   val qconsts_lookup: theory -> term -> qconsts_info     (* raises NotFound *)
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory
   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
-  val qconsts_dest: theory -> qconsts_info list
+  val qconsts_dest: Proof.context -> qconsts_info list
   val print_qconstinfo: Proof.context -> unit
 
   val equiv_rules_get: Proof.context -> thm list
@@ -198,8 +198,8 @@
 fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo))
 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I
 
-fun qconsts_dest thy =
-  flat (map snd (Symtab.dest (QConstsData.get thy)))
+fun qconsts_dest lthy =
+  flat (map snd (Symtab.dest (QConstsData.get (ProofContext.theory_of lthy))))
 
 fun qconsts_lookup thy t =
   let
diff -r 2a19e0a37131 -r 4163fe3dbf8c Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Thu Jan 14 10:47:19 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 14 10:51:03 2010 +0100
@@ -503,9 +503,7 @@
 *)
 fun clean_tac lthy =
 let
-  (* FIXME/TODO produce defs with lthy, like prs and ids *)
-  val thy = ProofContext.theory_of lthy;
-  val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+  val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest lthy)
   (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
   val prs = prs_rules_get lthy
   val ids = id_simps_get lthy