src/Pure/Isar/expression.ML
changeset 51728 0f6e8c4144a5
parent 51727 cf97bb5bbc90
child 51729 106bd5a4af22
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
     1.3 @@ -897,12 +897,11 @@
     1.4    let
     1.5      val facts =
     1.6        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
     1.7 -    val (eqns', _) = ctxt (* FIXME duplication to add_thmss *)
     1.8 -      |> Attrib.local_notes Thm.lemmaK facts
     1.9 +    val (eqns', ctxt') = ctxt
    1.10 +      |> Local_Theory.notes_kind Thm.lemmaK facts
    1.11        |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts')));
    1.12    in
    1.13 -    ctxt
    1.14 -    |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts)
    1.15 +    ctxt'
    1.16      |> Proof_Context.background_theory (fold2 (fn (dep, morph) => fn wits =>
    1.17        fn thy =>
    1.18          Locale.add_dependency target