prop_tr': proper handling of aprop marked as bound;

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