TFL/post.ML

  * Extract termination goals so that they can be put it into a goalstack, or
  * have a tactic directly applied to them.
  *--------------------------------------------------------------------------*)
 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
  * puts them into a goalstack.
  *--------------------------------------------------------------------------*)