# HG changeset patch
# User haftmann
# Date 1366533678 -7200
# Node ID 0f6e8c4144a57137dcad16806d20b7f97d2d9e61
# Parent  cf97bb5bbc90c901c70166c56b495e0ba935407e
avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target

diff -r cf97bb5bbc90 -r 0f6e8c4144a5 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
@@ -897,12 +897,11 @@
   let
     val facts =
       (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
-    val (eqns', _) = ctxt (* FIXME duplication to add_thmss *)
-      |> Attrib.local_notes Thm.lemmaK facts
+    val (eqns', ctxt') = ctxt
+      |> Local_Theory.notes_kind Thm.lemmaK facts
       |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts')));
   in
-    ctxt
-    |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts)
+    ctxt'
     |> Proof_Context.background_theory (fold2 (fn (dep, morph) => fn wits =>
       fn thy =>
         Locale.add_dependency target