--- a/src/HOL/Nominal/nominal_primrec.ML Sat Jan 14 16:58:29 2012 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Sat Jan 14 17:45:04 2012 +0100
@@ -332,7 +332,7 @@
val cprems = map cert prems;
val asms = map Thm.assume cprems;
val premss = map (fn (cargs, eprems, eqn) =>
- map (fn t => list_all_free (cargs, Logic.list_implies (eprems, t)))
+ map (fn t => fold_rev (Logic.all o Free) cargs (Logic.list_implies (eprems, t)))
(List.drop (prems_of eqn, length prems))) rec_rewrites';
val cpremss = map (map cert) premss;
val asmss = map (map Thm.assume) cpremss;
@@ -355,7 +355,7 @@
(Conjunction.intr_balanced (map mk_eqn (rec_rewrites' ~~ asmss)));
val goals = map (fn ((cargs, _, _), eqn) =>
- (list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns');
+ (fold_rev (Logic.all o Free) cargs eqn, [])) (rec_rewrites' ~~ eqns');
in
lthy' |>