1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Apr 19 14:57:09 2011 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Apr 19 15:58:05 2011 +0200
     1.3 @@ -275,10 +275,8 @@
     1.4    Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
     1.5  
     1.6  fun simple_check eq f xs ctxt =
     1.7 -  let val xs' = f ctxt xs in
     1.8 -    if pointer_eq (xs, xs') orelse eq_list eq (xs, xs') then NONE
     1.9 -    else SOME (xs', ctxt)
    1.10 -  end;
    1.11 +  let val xs' = f ctxt xs
    1.12 +  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
    1.13  
    1.14  in
    1.15