src/HOL/Set.thy

--- a/src/HOL/Set.thy	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Set.thy	Wed Aug 17 18:05:31 2011 +0200
@@ -281,7 +281,7 @@
         val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
         val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
         val exP = ex_tr [idts, P];
-      in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
+      in Syntax.const @{const_syntax Collect} $ absdummy dummyT exP end;
 
   in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
 *}