Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target
authorhaftmann
Sun, 21 Apr 2013 10:41:18 +0200
changeset 51728 0f6e8c4144a5
parent 51727 cf97bb5bbc90
child 51729 106bd5a4af22
avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target
src/Pure/Isar/expression.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle