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.
Term.absdummy;
authorwenzelm
Fri, 07 Oct 2005 22:59:22 +0200
changeset 17784 5cbb52f2c478
parent 17783 4175daa1286c
child 17785 8d928051d6a7
Term.absdummy;
src/HOL/Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Set.thy	Fri Oct 07 22:59:21 2005 +0200
+++ b/src/HOL/Set.thy	Fri Oct 07 22:59:22 2005 +0200
@@ -251,7 +251,7 @@
         val eq = Syntax.const "op =" $ Bound (nvars idts) $ e;
         val P = Syntax.const "op &" $ eq $ b;
         val exP = ex_tr [idts, P];
-      in Syntax.const "Collect" $ Abs ("", dummyT, exP) end;
+      in Syntax.const "Collect" $ Term.absdummy (dummyT, exP) end;
 
   in [("@SetCompr", setcompr_tr)] end;
 *}
isabelle