# HG changeset patch # User blanchet # Date 1307542818 -7200 # Node ID 0271fda2a83af65760a0ae8d00d97f029f2840e6 # Parent a80cdc4b27a308309d4e89f3cbee1d19d110c9a9 restore comment about subtle issue diff -r a80cdc4b27a3 -r 0271fda2a83a src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 16:20:18 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 16:20:18 2011 +0200 @@ -230,7 +230,8 @@ (* Match untyped terms. *) fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b) | untyped_aconv (Free (a, _), Free (b, _)) = (a = b) - | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = (a = b) + | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = + (a = b) (* ignore variable numbers *) | untyped_aconv (Bound i, Bound j) = (i = j) | untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u) | untyped_aconv (t1 $ t2, u1 $ u2) =