# HG changeset patch
# User wenzelm
# Date 1128718762 -7200
# Node ID 5cbb52f2c478baa5bef24d932582f215000e4be2
# Parent  4175daa1286c9f03066132c96a5a0547f684fd0d
Term.absdummy;

diff -r 4175daa1286c -r 5cbb52f2c478 src/HOL/Set.thy
--- 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;
 *}