915 | @{const_name finite} => |
915 | @{const_name finite} => |
916 let |
916 let |
917 val M1 = mtype_for (domain_type (domain_type T)) |
917 val M1 = mtype_for (domain_type (domain_type T)) |
918 val a = if exists_alpha_sub_mtype M1 then Fls else Gen |
918 val a = if exists_alpha_sub_mtype M1 then Fls else Gen |
919 in (MFun (MFun (M1, A a, bool_M), A Gen, bool_M), accum) end |
919 in (MFun (MFun (M1, A a, bool_M), A Gen, bool_M), accum) end |
920 | @{const_name Sigma} => |
920 | @{const_name prod} => |
921 let |
921 let |
922 val x = Unsynchronized.inc max_fresh |
922 val x = Unsynchronized.inc max_fresh |
923 fun mtype_for_set T = |
923 fun mtype_for_set T = |
924 MFun (mtype_for (domain_type T), V x, bool_M) |
924 MFun (mtype_for (domain_type T), V x, bool_M) |
925 val a_set_T = domain_type T |
925 val a_set_M = mtype_for_set (domain_type T) |
926 val a_M = mtype_for (domain_type a_set_T) |
|
927 val b_set_M = |
926 val b_set_M = |
928 mtype_for_set (range_type (domain_type (range_type T))) |
927 mtype_for_set (range_type (domain_type (range_type T))) |
929 val a_set_M = mtype_for_set a_set_T |
|
930 val a_to_b_set_M = MFun (a_M, A Gen, b_set_M) |
|
931 val ab_set_M = mtype_for_set (nth_range_type 2 T) |
928 val ab_set_M = mtype_for_set (nth_range_type 2 T) |
932 in |
929 in |
933 (MFun (a_set_M, A Gen, MFun (a_to_b_set_M, A Gen, ab_set_M)), |
930 (MFun (a_set_M, A Gen, MFun (b_set_M, A Gen, ab_set_M)), |
934 accum ||> add_annotation_atom_comp Neq [] (V x) (A New)) |
931 accum ||> add_annotation_atom_comp Neq [] (V x) (A New)) |
935 end |
932 end |
936 | _ => |
933 | _ => |
937 if s = @{const_name safe_The} then |
934 if s = @{const_name safe_The} then |
938 let |
935 let |