# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263386447 -3600
# Node ID e3d17c4b3eca0c1cb284fb43add52fcc18ba01b0
# Parent  e18c691335db660ebc49f949d1531898bdba2e52# Parent  adadd069647283b6158039ae2df521d986f16648
merged

diff -r adadd0696472 -r e3d17c4b3eca Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Wed Jan 13 13:12:04 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 13 13:40:47 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