393 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
393 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
394 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
394 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
395 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
395 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
396 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
396 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
397 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
397 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
398 val thy = Local_Theory.exit_global lthy2; |
398 |
|
399 val (_, lthy2a) = Local_Theory.note ((Binding.empty, |
|
400 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2; |
|
401 val thy = Local_Theory.exit_global lthy2a; |
399 val thy_name = Context.theory_name thy |
402 val thy_name = Context.theory_name thy |
400 |
403 |
401 val lthy3 = Theory_Target.init NONE thy; |
404 val lthy3 = Theory_Target.init NONE thy; |
402 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
405 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
403 |
406 |