TFL/rules.ML

--- a/TFL/rules.ML	Fri Mar 04 11:44:26 2005 +0100
+++ b/TFL/rules.ML	Fri Mar 04 15:07:34 2005 +0100
@@ -133,8 +133,8 @@
 
 fun FILTER_DISCH_ALL P thm =
  let fun check tm = P (#t (Thm.rep_cterm tm))
- in  Library.foldr (fn (tm,th) => if check tm then DISCH tm th else th)
-              (chyps thm, thm)
+ in  foldr (fn (tm,th) => if check tm then DISCH tm th else th)
+              thm (chyps thm)
  end;
 
 (* freezeT expensive! *)