621 if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) |
621 if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) |
622 else pair (alternate_disc k, alternate_disc_no_def) |
622 else pair (alternate_disc k, alternate_disc_no_def) |
623 else if Binding.eq_name (b, equal_binding) then |
623 else if Binding.eq_name (b, equal_binding) then |
624 pair (Term.lambda u exist_xs_u_eq_ctr, refl) |
624 pair (Term.lambda u exist_xs_u_eq_ctr, refl) |
625 else |
625 else |
626 Specification.definition (SOME (b, NONE, NoSyn)) [] |
626 Specification.definition (SOME (b, NONE, NoSyn)) [] [] |
627 ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd) |
627 ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd) |
628 ks exist_xs_u_eq_ctrs disc_bindings |
628 ks exist_xs_u_eq_ctrs disc_bindings |
629 ||>> apfst split_list o fold_map (fn (b, proto_sels) => |
629 ||>> apfst split_list o fold_map (fn (b, proto_sels) => |
630 Specification.definition (SOME (b, NONE, NoSyn)) [] |
630 Specification.definition (SOME (b, NONE, NoSyn)) [] [] |
631 ((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos |
631 ((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos |
632 ||> `Local_Theory.close_target; |
632 ||> `Local_Theory.close_target; |
633 |
633 |
634 val phi = Proof_Context.export_morphism lthy lthy'; |
634 val phi = Proof_Context.export_morphism lthy lthy'; |
635 |
635 |