diff -r cf53c2dcf440 -r b1d1b5bfc464 TFL/post.ML
--- a/TFL/post.ML	Fri Mar 04 11:44:26 2005 +0100
+++ b/TFL/post.ML	Fri Mar 04 15:07:34 2005 +0100
@@ -46,7 +46,7 @@
  *--------------------------------------------------------------------------*)
 fun termination_goals rules =
     map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
-      (Library.foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
+      (foldr (fn (th,A) => union_term (prems_of th, A)) [] rules);
 
 (*---------------------------------------------------------------------------
  * Finds the termination conditions in (highly massaged) definition and