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;
 *}