Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mark_boundT: produce well-typed term;
authorwenzelm
Tue, 21 Mar 2006 12:18:22 +0100
changeset 19311 e3d48fa3908e
parent 19310 9b2080d9ed28
child 19312 bb3cbf03a021
mark_boundT: produce well-typed term;
src/Pure/Syntax/syn_trans.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle