# HG changeset patch
# User wenzelm
# Date 1518980901 -3600
# Node ID 8f4810b9d9d1afffa7a532249f1b0ef34fe7f5dd
# Parent  49f45fcd335b7a8ee9491745c21830659921e914
tuned;

diff -r 49f45fcd335b -r 8f4810b9d9d1 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Feb 18 19:49:01 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Feb 18 20:08:21 2018 +0100
@@ -583,29 +583,24 @@
 
 (*** Storing results ***)
 
-(* Theorems *)
-
 fun add_facts loc kind facts ctxt =
   if null facts then ctxt
   else
     let
-      val stored_notes = ((kind, map Attrib.trim_context_fact facts), serial ());
+      val notes = ((kind, map Attrib.trim_context_fact facts), serial ());
 
       fun global_notes morph thy = thy
-        |> (snd o Attrib.global_notes kind
-            (Attrib.transform_facts (Morphism.transfer_morphism thy $> morph) facts));
-      fun registrations 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;
     in
       ctxt
-      |> Attrib.local_notes kind facts |> snd
+      |> Attrib.local_notes kind facts |> #2
       |> Proof_Context.background_theory
-        ((change_locale loc o apfst o apsnd) (cons stored_notes) #> registrations)
+        ((change_locale loc o apfst o apsnd) (cons notes) #> apply_registrations)
     end;
 
-
-(* Declarations *)
-
 fun add_declaration loc syntax decl =
   syntax ?
     Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))