--- a/Quot/quotient_tacs.ML	Thu Jan 14 12:14:35 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 14 12:17:39 2010 +0100
@@ -57,7 +57,7 @@
 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
-fun quotient_tac ctxt = SOLVED'
+fun quotient_tac ctxt =
   (REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
      resolve_tac (quotient_rules_get ctxt)]))
@@ -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