mark_boundT: produce well-typed term;
authorwenzelm
Tue Mar 21 12:18:22 2006 +0100 (2006-03-21)
changeset 19311e3d48fa3908e
parent 19310 9b2080d9ed28
child 19312 bb3cbf03a021
mark_boundT: produce well-typed term;
src/Pure/Syntax/syn_trans.ML
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Mar 21 12:18:21 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Mar 21 12:18:22 2006 +0100
     1.3 @@ -234,7 +234,7 @@
     1.4  
     1.5  (* abstraction *)
     1.6  
     1.7 -fun mark_boundT x_T = Lexicon.const "_bound" $ Free x_T;
     1.8 +fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
     1.9  fun mark_bound x = mark_boundT (x, dummyT);
    1.10  
    1.11  fun bound_vars vars body =