diff -r 04f0e4ca1451 -r b15981aedb7b TFL/post.ML
--- a/TFL/post.ML	Wed Nov 09 16:26:53 2005 +0100
+++ b/TFL/post.ML	Wed Nov 09 16:26:54 2005 +0100
@@ -43,7 +43,7 @@
  *--------------------------------------------------------------------------*)
 fun termination_goals rules =
     map (Type.freeze o HOLogic.dest_Trueprop)
-      (foldr (fn (th,A) => union_term (prems_of th, A)) [] rules);
+      (foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules);
 
 (*---------------------------------------------------------------------------
  * Finds the termination conditions in (highly massaged) definition and