changeset 42403 | 38b29c9fc742 |
parent 42402 | c7139609b67d |
child 42408 | 282b7a3065d3 |
--- 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