# HG changeset patch
# User blanchet
# Date 1276539396 -7200
# Node ID 0714ece4908179280985209ecc5d5fbd48ca7d0e
# Parent  d5ac8280497e1e8e09a7fb3ce76ec4312d5c90f7
A function called "untyped_aconv" shouldn't look at the bound names!

diff -r d5ac8280497e -r 0714ece49081 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Jun 14 19:20:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Jun 14 20:16:36 2010 +0200
@@ -44,14 +44,16 @@
 (* Useful Functions                                                          *)
 (* ------------------------------------------------------------------------- *)
 
-(* 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)   (*the index is ignored!*)
-  | untyped_aconv (Bound i)      (Bound j)      = (i=j)
-  | untyped_aconv (Abs(a,_,t))  (Abs(b,_,u))    = (a=b) andalso untyped_aconv t u
-  | untyped_aconv (t1$t2) (u1$u2)  = untyped_aconv t1 u1 andalso untyped_aconv t2 u2
-  | untyped_aconv _              _              = false;
+(* 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) (* The index is ignored, for some reason. *)
+  | untyped_aconv (Bound i) (Bound j) = (i = j)
+  | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
+  | untyped_aconv (t1 $ t2) (u1 $ u2) =
+    untyped_aconv t1 u1 andalso untyped_aconv t2 u2
+  | untyped_aconv _ _ = false
 
 (* Finding the relative location of an untyped term within a list of terms *)
 fun get_index lit =