1.1 --- a/src/HOL/Tools/record.ML	Sat Jan 14 19:06:05 2012 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Jan 14 20:05:58 2012 +0100
     1.3 @@ -1121,7 +1121,7 @@
     1.4                  SOME (trm, trm', vars) =>
     1.5                    SOME
     1.6                      (prove_unfold_defs thy [] []
     1.7 -                      (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
     1.8 +                      (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
     1.9                | NONE => NONE)
    1.10              end
    1.11            else NONE
    1.12 @@ -1249,7 +1249,7 @@
    1.13          if simp then
    1.14            SOME
    1.15              (prove_unfold_defs thy noops' [simproc]
    1.16 -              (list_all (vars, Logic.mk_equals (lhs, rhs))))
    1.17 +              (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
    1.18          else NONE
    1.19        end);
    1.20  
    1.21 @@ -1345,7 +1345,7 @@
    1.22             (let
    1.23               val eq = mkeq (dest_sel_eq t) 0;
    1.24               val prop =
    1.25 -               list_all ([("r", T)],
    1.26 +               Logic.list_all ([("r", T)],
    1.27                   Logic.mk_equals
    1.28                    (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
    1.29              in