equal
deleted
inserted
replaced
211 map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
211 map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
212 end |
212 end |
213 |
213 |
214 fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy = |
214 fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy = |
215 let |
215 let |
|
216 val _ = tracing ("bclausesss\n" ^ cat_lines (map (cat_lines o map PolyML.makestring) bclausesss)) |
|
217 |
216 val fv_names = prefix_dt_names descr sorts "fv_" |
218 val fv_names = prefix_dt_names descr sorts "fv_" |
217 val fv_arg_tys = all_dtyps descr sorts |
219 val fv_arg_tys = all_dtyps descr sorts |
218 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; |
220 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; |
219 val fv_frees = map Free (fv_names ~~ fv_tys); |
221 val fv_frees = map Free (fv_names ~~ fv_tys); |
220 val fv_map = fv_arg_tys ~~ fv_frees |
222 val fv_map = fv_arg_tys ~~ fv_frees |