# HG changeset patch
# User wenzelm
# Date 1142939902 -3600
# Node ID e3d48fa3908e69ebe32a491230ea974f421792c4
# Parent  9b2080d9ed282d3afe2f1bdcf6ab25ed43d9fd4c
mark_boundT: produce well-typed term;

diff -r 9b2080d9ed28 -r e3d48fa3908e src/Pure/Syntax/syn_trans.ML
--- 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 =