equal
deleted
inserted
replaced
322 |
322 |
323 fun is_prop Ts t = |
323 fun is_prop Ts t = |
324 fastype_of1 (Ts, t) = propT handle TERM _ => false; |
324 fastype_of1 (Ts, t) = propT handle TERM _ => false; |
325 |
325 |
326 fun tr' _ (t as Const _) = t |
326 fun tr' _ (t as Const _) = t |
|
327 | tr' Ts (t as Const ("_bound", _) $ u) = |
|
328 if is_prop Ts u then aprop t else t |
327 | tr' _ (t as Free (x, T)) = |
329 | tr' _ (t as Free (x, T)) = |
328 if T = propT then aprop (Lexicon.free x) else t |
330 if T = propT then aprop (Lexicon.free x) else t |
329 | tr' _ (t as Var (xi, T)) = |
331 | tr' _ (t as Var (xi, T)) = |
330 if T = propT then aprop (Lexicon.var xi) else t |
332 if T = propT then aprop (Lexicon.var xi) else t |
331 | tr' Ts (t as Bound _) = |
333 | tr' Ts (t as Bound _) = |