71 if Datatype_Aux.is_rec_type dt |
71 if Datatype_Aux.is_rec_type dt |
72 then nth fv_frees (Datatype_Aux.body_index dt) |
72 then nth fv_frees (Datatype_Aux.body_index dt) |
73 else Const (@{const_name supp}, |
73 else Const (@{const_name supp}, |
74 Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ "atom set"}) |
74 Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ "atom set"}) |
75 val fvs = map fv_for_dt body_dts; |
75 val fvs = map fv_for_dt body_dts; |
76 val fv = mk_compound_fv fvs; |
76 val fv = mk_compound_fv' lthy fvs; |
77 fun alpha_for_dt dt = |
77 fun alpha_for_dt dt = |
78 if Datatype_Aux.is_rec_type dt |
78 if Datatype_Aux.is_rec_type dt |
79 then nth alpha_frees (Datatype_Aux.body_index dt) |
79 then nth alpha_frees (Datatype_Aux.body_index dt) |
80 else Const (@{const_name "op ="}, |
80 else Const (@{const_name "op ="}, |
81 Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> |
81 Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> |
82 Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ bool}) |
82 Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ bool}) |
83 val alphas = map alpha_for_dt body_dts; |
83 val alphas = map alpha_for_dt body_dts; |
84 val alpha = mk_compound_alpha alphas; |
84 val alpha = mk_compound_alpha' lthy alphas; |
85 val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs |
85 val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs |
86 val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre) |
86 val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre) |
87 val t = Syntax.check_term lthy alpha_gen_ex |
87 val t = Syntax.check_term lthy alpha_gen_ex |
88 in |
88 in |
89 case binds of |
89 case binds of |