equal
deleted
inserted
replaced
179 map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
179 map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
180 end |
180 end |
181 *} |
181 *} |
182 |
182 |
183 ML {* |
183 ML {* |
184 fun define_raw_alpha descr sorts bn_info bclausesss fvs fv_bns lthy = |
184 fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy = |
185 let |
185 let |
186 val alpha_names = prefix_dt_names descr sorts "alpha_" |
186 val alpha_names = prefix_dt_names descr sorts "alpha_" |
187 val alpha_arg_tys = all_dtyps descr sorts |
187 val alpha_arg_tys = all_dtyps descr sorts |
188 val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys |
188 val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys |
189 val alpha_frees = map Free (alpha_names ~~ alpha_tys) |
189 val alpha_frees = map Free (alpha_names ~~ alpha_tys) |
224 in |
224 in |
225 (alpha_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
225 (alpha_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
226 end |
226 end |
227 *} |
227 *} |
228 |
228 |
229 ML {* ProofContext.export_morphism *} |
229 end |
230 |
|
231 end |
|