equal
deleted
inserted
replaced
275 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
275 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
276 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
276 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
277 val thy = Local_Theory.exit_global lthy2; |
277 val thy = Local_Theory.exit_global lthy2; |
278 val lthy3 = Theory_Target.init NONE thy; |
278 val lthy3 = Theory_Target.init NONE thy; |
279 |
279 |
280 val (_, lthy4) = define_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
280 val (_, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
281 in |
281 in |
282 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4) |
282 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4) |
283 end |
283 end |
284 *} |
284 *} |
285 |
285 |