--- 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