diff -r c7139609b67d -r 38b29c9fc742 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Apr 19 14:57:09 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Apr 19 15:58:05 2011 +0200
@@ -275,10 +275,8 @@
   Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
 
 fun simple_check eq f xs ctxt =
-  let val xs' = f ctxt xs in
-    if pointer_eq (xs, xs') orelse eq_list eq (xs, xs') then NONE
-    else SOME (xs', ctxt)
-  end;
+  let val xs' = f ctxt xs
+  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
 
 in