# HG changeset patch
# User wenzelm
# Date 1519160644 -3600
# Node ID b5058ba95e32133e449fcb86b2bfdf86d5e5fc09
# Parent  738f170f43ee4977ea138b3224c0b1a50e1bc1a4# Parent  175a070e9dd86fb4cf88de5b6eb3fde9c16037b5
merged

diff -r 738f170f43ee -r b5058ba95e32 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Feb 20 09:34:03 2018 +0000
+++ b/src/Pure/Isar/locale.ML	Tue Feb 20 22:04:04 2018 +0100
@@ -418,18 +418,20 @@
 
 (* Potentially lazy notes *)
 
+fun make_notes kind = map (fn ((b, atts), facts) =>
+  if null atts andalso forall (null o #2) facts
+  then Lazy_Notes (kind, (b, Lazy.value (maps #1 facts)))
+  else Notes (kind, [((b, atts), facts)]));
+
 fun lazy_notes thy loc =
-  rev (#notes (the_locale thy loc)) |> maps (fn ((kind, notes), _) =>
-    notes |> map (fn ((b, atts), facts) =>
-      if null atts andalso forall (null o #2) facts andalso false (* FIXME *)
-      then Lazy_Notes (kind, (b, Lazy.value (maps #1 facts)))
-      else Notes (kind, [((b, atts), facts)])));
+  rev (#notes (the_locale thy loc))
+  |> maps (fn ((kind, notes), _) => make_notes kind notes);
 
 fun consolidate_notes elems =
-  (elems
-    |> map_filter (fn Lazy_Notes (_, (_, ths)) => SOME ths | _ => NONE)
-    |> Lazy.consolidate;
-   elems);
+  elems
+  |> map_filter (fn Lazy_Notes (_, (_, ths)) => SOME ths | _ => NONE)
+  |> Lazy.consolidate
+  |> ignore;
 
 fun force_notes (Lazy_Notes (kind, (b, ths))) = Notes (kind, [((b, []), [(Lazy.force ths, [])])])
   | force_notes elem = elem;
@@ -455,7 +457,7 @@
         NONE => Morphism.identity
       | SOME export => collect_mixins context (name, morph $> export) $> export);
     val morph' = transfer input $> morph $> mixin;
-    val notes' = grouped 100 Par_List.map (Element.transform_ctxt morph') (lazy_notes thy name);
+    val notes' = map (Element.transform_ctxt morph') (lazy_notes thy name);
   in
     (notes', input) |-> fold (fn elem => fn res =>
       activ_elem (Element.transform_ctxt (transfer res) elem) res)
@@ -611,18 +613,19 @@
   if null facts then ctxt
   else
     let
-      val notes = ((kind, map Attrib.trim_context_fact facts), serial ());
+      val stored_notes = ((kind, map Attrib.trim_context_fact facts), serial ());
+      val applied_notes = make_notes kind facts;
 
-      fun global_notes morph thy = thy
-        |> Attrib.global_notes kind
-            (Attrib.transform_facts (Morphism.transfer_morphism thy $> morph) facts) |> #2;
-      fun apply_registrations thy =
-        fold_rev (global_notes o #2) (registrations_of (Context.Theory thy) loc) thy;
+      fun apply_notes morph = applied_notes |> fold (fn elem => fn context =>
+        let val elem' = Element.transform_ctxt (Morphism.transfer_morphism'' context $> morph) elem
+        in Element.init elem' context end);
+      val apply_registrations = Context.theory_map (fn context =>
+        fold_rev (apply_notes o #2) (registrations_of context loc) context);
     in
       ctxt
       |> Attrib.local_notes kind facts |> #2
       |> Proof_Context.background_theory
-        ((change_locale loc o apfst o apsnd) (cons notes) #> apply_registrations)
+        ((change_locale loc o apfst o apsnd) (cons stored_notes) #> apply_registrations)
     end;
 
 fun add_declaration loc syntax decl =
@@ -703,7 +706,7 @@
     val elems =
       activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, [])
       |> snd |> rev
-      |> consolidate_notes
+      |> tap consolidate_notes
       |> map force_notes;
   in
     Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
diff -r 738f170f43ee -r b5058ba95e32 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Feb 20 09:34:03 2018 +0000
+++ b/src/Pure/Isar/proof_context.ML	Tue Feb 20 22:04:04 2018 +0100
@@ -125,6 +125,7 @@
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
+  val is_stmt: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
   val restore_stmt: Proof.context -> Proof.context -> Proof.context
   val add_thms_dynamic: binding * (Context.generic -> thm list) ->
diff -r 738f170f43ee -r b5058ba95e32 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Tue Feb 20 09:34:03 2018 +0000
+++ b/src/Pure/facts.ML	Tue Feb 20 22:04:04 2018 +0100
@@ -269,8 +269,10 @@
     val (name, facts') =
       if Binding.is_empty b then ("", facts)
       else Name_Space.define context strict (b, Static ths') facts;
-    val props' = props
-      |> index ? fold (add_prop (Binding.pos_of (Binding.default_pos b))) (Lazy.force ths');
+    val props' =
+      if index then
+        props |> fold (add_prop (Binding.pos_of (Binding.default_pos b))) (Lazy.force ths')
+      else props;
   in (name, make_facts facts' props') end;
 
 fun add_dynamic context (b, f) (Facts {facts, props}) =
diff -r 738f170f43ee -r b5058ba95e32 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Tue Feb 20 09:34:03 2018 +0000
+++ b/src/Pure/global_theory.ML	Tue Feb 20 22:04:04 2018 +0100
@@ -116,8 +116,8 @@
   |> (if name = "" orelse pre andalso Thm.has_name_hint thm then I
       else Thm.put_name_hint name);
 
-fun name_thms pre official name xs =
-  map (uncurry (name_thm pre official)) (name_multi name xs);
+fun name_thms pre official name thms =
+  map (uncurry (name_thm pre official)) (name_multi name thms);
 
 fun name_thmss official name fact =
   burrow_fact (name_thms true official name) fact;