--- a/src/HOL/Tools/TFL/post.ML Wed Oct 21 12:02:19 2009 +0200
+++ b/src/HOL/Tools/TFL/post.ML Wed Oct 21 12:02:56 2009 +0200
@@ -28,7 +28,7 @@
*--------------------------------------------------------------------------*)
fun termination_goals rules =
map (Type.freeze o HOLogic.dest_Trueprop)
- (List.foldr (fn (th,A) => union (op aconv) (prems_of th, A)) [] rules);
+ (List.foldr (fn (th,A) => uncurry (union (op aconv)) (prems_of th, A)) [] rules);
(*---------------------------------------------------------------------------
* Three postprocessors are applied to the definition. It
@@ -79,7 +79,7 @@
val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *)
val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *)
- val cntxt = union (op aconv) (cntxtl, cntxtr)
+ val cntxt = union (op aconv) cntxtl cntxtr
in
R.GEN_ALL
(R.DISCH_ALL