# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263386423 -3600
# Node ID e18c691335db660ebc49f949d1531898bdba2e52
# Parent  bb012513fb39a292916d52bb4b380b5821f6aa32
deleted SOLVED'

diff -r bb012513fb39 -r e18c691335db Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Wed Jan 13 09:41:57 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 13 13:40:23 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