# 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) =