276 let |
276 let |
277 val thy = ProofContext.theory_of lthy |
277 val thy = ProofContext.theory_of lthy |
278 val thy_name = Context.theory_name thy |
278 val thy_name = Context.theory_name thy |
279 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = |
279 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = |
280 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
280 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
281 val bn_funs_decls = []; |
|
282 |
|
283 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
281 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
|
282 val raw_bns_exp = map (apsnd (map (apfst (Morphism.term morphism_2_1)))) raw_bns; |
|
283 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
|
284 |
284 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
285 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
285 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
286 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
286 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
287 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
287 val descr = #descr dtinfo; |
288 val descr = #descr dtinfo; |
288 val sorts = #sorts dtinfo; |
289 val sorts = #sorts dtinfo; |