src/HOL/Tools/record.ML

             in
               (case mk_eq_terms (upd $ k $ r) of
                 SOME (trm, trm', vars) =>
                   SOME
                     (prove_unfold_defs thy [] []
-                      (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
+                      (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
               | NONE => NONE)
             end
           else NONE
       | _ => NONE));
 

         val noops' = maps snd (Symtab.dest noops);
       in
         if simp then
           SOME
             (prove_unfold_defs thy noops' [simproc]
-              (list_all (vars, Logic.mk_equals (lhs, rhs))))
+              (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
         else NONE
       end);
 
 end;
 

         (case t of
           Const (@{const_name Ex}, Tex) $ Abs (s, T, t) =>
            (let
              val eq = mkeq (dest_sel_eq t) 0;
              val prop =
-               list_all ([("r", T)],
+               Logic.list_all ([("r", T)],
                  Logic.mk_equals
                   (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
             in
               SOME (Skip_Proof.prove_global thy [] [] prop
                 (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)