equal
deleted
inserted
replaced
895 |
895 |
896 fun note_eqns_dependency target deps witss attrss eqns export export' ctxt = |
896 fun note_eqns_dependency target deps witss attrss eqns export export' ctxt = |
897 let |
897 let |
898 val facts = |
898 val facts = |
899 (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns); |
899 (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns); |
900 val (eqns', _) = ctxt (* FIXME duplication to add_thmss *) |
900 val (eqns', ctxt') = ctxt |
901 |> Attrib.local_notes Thm.lemmaK facts |
901 |> Local_Theory.notes_kind Thm.lemmaK facts |
902 |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts'))); |
902 |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts'))); |
903 in |
903 in |
904 ctxt |
904 ctxt' |
905 |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts) |
|
906 |> Proof_Context.background_theory (fold2 (fn (dep, morph) => fn wits => |
905 |> Proof_Context.background_theory (fold2 (fn (dep, morph) => fn wits => |
907 fn thy => |
906 fn thy => |
908 Locale.add_dependency target |
907 Locale.add_dependency target |
909 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)) |
908 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)) |
910 (Element.eq_morphism thy eqns' |> Option.map (rpair true)) |
909 (Element.eq_morphism thy eqns' |> Option.map (rpair true)) |