# HG changeset patch
# User wenzelm
# Date 1135207750 -3600
# Node ID 29a5070b517c76c77e66ee5293190fe88104fbc7
# Parent  bf2a02c82a55a4e51fdcca4d5d25cb51227ed01c
prop_tr': proper handling of aprop marked as bound;

diff -r bf2a02c82a55 -r 29a5070b517c src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Thu Dec 22 00:29:09 2005 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Thu Dec 22 00:29:10 2005 +0100
@@ -324,6 +324,8 @@
       fastype_of1 (Ts, t) = propT handle TERM _ => false;
 
     fun tr' _ (t as Const _) = t
+      | tr' Ts (t as Const ("_bound", _) $ u) =
+          if is_prop Ts u then aprop t else t
       | tr' _ (t as Free (x, T)) =
           if T = propT then aprop (Lexicon.free x) else t
       | tr' _ (t as Var (xi, T)) =