--- a/Quot/quotient_tacs.ML	Thu Jan 14 10:06:29 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 14 10:47:19 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)]))