# HG changeset patch
# User wenzelm
# Date 1132406469 -3600
# Node ID 1945ae1668d20410fca09097e4ab93e7cbbdf61b
# Parent  8f3973d3b2f0af897432c0bf6f345693d3b631fc
tuned;

diff -r 8f3973d3b2f0 -r 1945ae1668d2 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Sat Nov 19 14:21:08 2005 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Sat Nov 19 14:21:09 2005 +0100
@@ -363,7 +363,7 @@
       [Abs (_, _, Const ("==>", _) $
         (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ (Const ("_aprop", _) $ Bound 0))) $
         (Const ("_aprop", _) $ Bound 0))] =
-      if 0 mem_int Term.loose_bnos A orelse 0 mem_int Term.loose_bnos B then raise Match
+      if Term.loose_bvar1 (A, 0) orelse Term.loose_bvar1 (B, 0) then raise Match
       else Lexicon.const "_meta_conjunction" $ A $ B
   | meta_conjunction_tr' (*"all"*) ts = raise Match;