src/HOL/Set.thy
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Set.thy	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Set.thy	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -268,7 +268,7 @@
     1.4  
     1.5      fun setcompr_tr [e, idts, b] =
     1.6        let
     1.7 -        val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
     1.8 +        val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
     1.9          val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
    1.10          val exP = ex_tr [idts, P];
    1.11        in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
    1.12 @@ -289,7 +289,7 @@
    1.13      let
    1.14        fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
    1.15          | check (Const (@{const_syntax HOL.conj}, _) $
    1.16 -              (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
    1.17 +              (Const (@{const_syntax HOL.eq}, _) $ Bound m $ e) $ P, n) =
    1.18              n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
    1.19              subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
    1.20          | check _ = false;