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]