src/HOL/Set.thy
changeset 44241 7943b69f0188
parent 43967 610efb6bda1f
child 44490 e3e8d20a6ebc
     1.1 --- a/src/HOL/Set.thy	Wed Aug 17 16:46:58 2011 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed Aug 17 18:05:31 2011 +0200
     1.3 @@ -281,7 +281,7 @@
     1.4          val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
     1.5          val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
     1.6          val exP = ex_tr [idts, P];
     1.7 -      in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
     1.8 +      in Syntax.const @{const_syntax Collect} $ absdummy dummyT exP end;
     1.9  
    1.10    in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
    1.11  *}