372 val induct = #induct dtinfo; |
372 val induct = #induct dtinfo; |
373 val exhausts = map #exhaust dtinfos; |
373 val exhausts = map #exhaust dtinfos; |
374 |
374 |
375 (* definitions of raw permutations *) |
375 (* definitions of raw permutations *) |
376 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
376 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
377 Local_Theory.theory_result (define_raw_perms dtinfo) lthy1; |
377 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; |
378 |
378 |
379 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
379 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
380 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
380 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
381 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
381 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
382 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
382 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |