diff -r 7b19666f0e3d -r ecf6375e2abb src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Sat Jan 14 19:06:05 2012 +0100
+++ b/src/Pure/primitive_defs.ML	Sat Jan 14 20:05:58 2012 +0100
@@ -64,7 +64,7 @@
     else if exists_subterm (fn t => t aconv head) rhs then
       err "Entity to be defined occurs on rhs"
     else
-      ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
+      ((lhs, rhs), fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
   end;
 
 (*!!x. c x == t[x] to c == %x. t[x]*)