src/HOL/Nominal/nominal_primrec.ML

 
     val prems = foldr1 (common_prefix op aconv) (map (prems_of o #3) rec_rewrites');
     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;
 
     fun mk_eqn ((cargs, eprems, eqn), asms') =

     val rule_prems = cprems @ flat cpremss;
     val rule = implies_intr_list rule_prems
       (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' |>
     Variable.add_fixes (map fst lsrs) |> snd |>
     Proof.theorem NONE