# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263392272 -3600
# Node ID 6a27fc81c42f65249bac8061498932be8f0d5833
# Parent  09ec51d50fc6327f175a60f7b463fad462543a34# Parent  e3d17c4b3eca0c1cb284fb43add52fcc18ba01b0
merge

diff -r 09ec51d50fc6 -r 6a27fc81c42f Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Wed Jan 13 15:17:36 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 13 15:17:52 2010 +0100
@@ -29,10 +29,6 @@
 (* composition of two theorems, used in maps *)
 fun OF1 thm1 thm2 = thm2 RS thm1
 
-(* 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 ((SOLVED' tac) i st) of