changeset 18478 | 29a5070b517c |
parent 18342 | 1b7109c10b7b |
child 18678 | dd0c569fa43d |
--- 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)) =