--- a/src/HOL/Nominal/nominal_permeq.ML Tue Oct 27 17:34:00 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Tue Oct 27 22:55:27 2009 +0100
@@ -301,9 +301,9 @@
val ps = Logic.strip_params (term_of goal);
val Ts = rev (map snd ps);
val vs = collect_vars 0 x [];
- val s = Library.foldr (fn (v, s) =>
+ val s = fold_rev (fn v => fn s =>
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
- (vs, HOLogic.unit);
+ vs HOLogic.unit;
val s' = list_abs (ps,
Const ("Nominal.supp", fastype_of1 (Ts, s) -->
snd (split_last (binder_types T)) --> HOLogic.boolT) $ s);
@@ -343,9 +343,9 @@
val ps = Logic.strip_params (term_of goal);
val Ts = rev (map snd ps);
val vs = collect_vars 0 t [];
- val s = Library.foldr (fn (v, s) =>
+ val s = fold_rev (fn v => fn s =>
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
- (vs, HOLogic.unit);
+ vs HOLogic.unit;
val s' = list_abs (ps,
Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;