| changeset 19311 | e3d48fa3908e |
| parent 19131 | 06b6f5f8e4cb |
| child 19473 | d87a8838afa4 |
--- a/src/Pure/Syntax/syn_trans.ML Tue Mar 21 12:18:21 2006 +0100 +++ b/src/Pure/Syntax/syn_trans.ML Tue Mar 21 12:18:22 2006 +0100 @@ -234,7 +234,7 @@ (* abstraction *) -fun mark_boundT x_T = Lexicon.const "_bound" $ Free x_T; +fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T); fun mark_bound x = mark_boundT (x, dummyT); fun bound_vars vars body =