501 let val rhs = Term.lambda u exist_xs_u_eq_ctr in |
501 let val rhs = Term.lambda u exist_xs_u_eq_ctr in |
502 if Binding.is_empty b then |
502 if Binding.is_empty b then |
503 if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) |
503 if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) |
504 else pair (alternate_disc k, alternate_disc_no_def) |
504 else pair (alternate_disc k, alternate_disc_no_def) |
505 else if Binding.eq_name (b, equal_binding) then |
505 else if Binding.eq_name (b, equal_binding) then |
506 pair (rhs, refl) |
506 pair (rhs, Thm.reflexive (certify lthy rhs)) |
507 else |
507 else |
508 Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) #>> apsnd snd |
508 Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) #>> apsnd snd |
509 end) ks exist_xs_u_eq_ctrs disc_bindings |
509 end) ks exist_xs_u_eq_ctrs disc_bindings |
510 ||>> apfst split_list o fold_map (fn (b, proto_sels) => |
510 ||>> apfst split_list o fold_map (fn (b, proto_sels) => |
511 Local_Theory.define ((b, NoSyn), |
511 Local_Theory.define ((b, NoSyn), |