--- a/src/Pure/unify.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/Pure/unify.ML Thu Oct 22 13:48:06 2009 +0200
@@ -531,12 +531,12 @@
Bound vars in the binder are "banned" unless used in both t AND u *)
fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) =
let val loot = loose_bnos t and loou = loose_bnos u
- fun add_index (((a,T), j), (bnos, newbinder)) =
+ fun add_index (j, (a,T)) (bnos, newbinder) =
if member (op =) loot j andalso member (op =) loou j
then (bnos, (a,T)::newbinder) (*needed by both: keep*)
else (j::bnos, newbinder); (*remove*)
- val indices = 0 upto (length rbinder - 1);
- val (banned,rbin') = List.foldr add_index ([],[]) (rbinder~~indices);
+ val (banned,rbin') = fold_rev add_index
+ ((0 upto (length rbinder - 1)) ~~ rbinder) ([],[]);
val (env', t') = clean_term banned (env, t);
val (env'',u') = clean_term banned (env',u)
in (ff_assign thy (env'', rbin', t', u'), tpairs)