diff -r 04f0e4ca1451 -r b15981aedb7b src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Wed Nov 09 16:26:53 2005 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Nov 09 16:26:54 2005 +0100
@@ -395,10 +395,10 @@
 fun antiquote_tr' name =
   let
     fun tr' i (t $ u) =
-      if u = Bound i then Lexicon.const name $ tr' i t
+      if u aconv Bound i then Lexicon.const name $ tr' i t
       else tr' i t $ tr' i u
       | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
-      | tr' i a = if a = Bound i then raise Match else a;
+      | tr' i a = if a aconv Bound i then raise Match else a;
   in tr' 0 end;
 
 fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)