diff -r 433f7c17255f -r 0ce025c02ef3 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Wed Jan 13 09:19:20 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 13 09:30:59 2010 +0100
@@ -29,12 +29,13 @@
 (* composition of two theorems, used in maps *)
 fun OF1 thm1 thm2 = thm2 RS thm1
 
-(* makes sure a subgoal is solved *)
-fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
+(* FIXME --- now in Isabelle *)
+fun SOLVED' tac i st =
+  tac i st |> Seq.filter (fn st' => nprems_of st' < nprems_of st)
 
 (* prints a warning, if the subgoal is not solved *)
 fun WARN (tac, msg) i st =
- case Seq.pull ((SOLVES' tac) i st) of
+ case Seq.pull ((SOLVED' tac) i st) of
      NONE    => (warning msg; Seq.single st)
    | seqcell => Seq.make (fn () => seqcell)
 
@@ -54,7 +55,7 @@
 
 (** solvers for equivp and quotient assumptions **)
 
-(* FIXME / TODO: should this SOLVES' the goal, like with quotient_tac? *)
+(* FIXME / TODO: should this SOLVED' the goal, like with quotient_tac? *)
 (* FIXME / TODO: none of te examples break if added                    *)
 fun equiv_tac ctxt =
   REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
@@ -64,7 +65,7 @@
 
 (* FIXME / TODO: test whether DETERM makes any runtime-difference *)
 (* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *)
-fun quotient_tac ctxt = SOLVES'
+fun quotient_tac ctxt = SOLVED'
   (REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
      resolve_tac (quotient_rules_get ctxt)]))