src/HOL/Set.thy
 changeset 46137 0477785525be parent 46128 53e7cc599f58 child 46146 6baea4fca6bd
```     1.1 --- a/src/HOL/Set.thy	Fri Jan 06 16:42:15 2012 +0100
1.2 +++ b/src/HOL/Set.thy	Fri Jan 06 16:45:19 2012 +0100
1.3 @@ -256,7 +256,6 @@
1.4
1.5  print_translation {*
1.6  let
1.7 -  val Type (set_type, _) = @{typ "'a set"};   (* FIXME 'a => bool (!?!) *)
1.8    val All_binder = Mixfix.binder_name @{const_syntax All};
1.9    val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
1.10    val impl = @{const_syntax HOL.implies};
1.11 @@ -275,14 +274,12 @@
1.12      then Syntax.const c \$ Syntax_Trans.mark_bound v' \$ n \$ P else raise Match;
1.13
1.14    fun tr' q = (q,
1.15 -        fn [Const (@{syntax_const "_bound"}, _) \$ Free (v, Type (T, _)),
1.16 +        fn [Const (@{syntax_const "_bound"}, _) \$ Free (v, Type (@{type_name set}, _)),
1.17              Const (c, _) \$
1.18                (Const (d, _) \$ (Const (@{syntax_const "_bound"}, _) \$ Free (v', _)) \$ n) \$ P] =>
1.19 -            if T = set_type then
1.20 -              (case AList.lookup (op =) trans (q, c, d) of
1.21 -                NONE => raise Match
1.22 -              | SOME l => mk v v' l n P)
1.23 -            else raise Match
1.24 +            (case AList.lookup (op =) trans (q, c, d) of
1.25 +              NONE => raise Match
1.26 +            | SOME l => mk v v' l n P)
1.27           | _ => raise Match);
1.28  in
1.29    [tr' All_binder, tr' Ex_binder]
```