# HG changeset patch
# User wenzelm
# Date 1518979285 -3600
# Node ID 4ba01fea9cfd852639d7ce4fc03e27e88290d841
# Parent  11716a084cae425836bfc77b4a249c706aa22775
misc tuning and clarification;
removed unused all_registrations_of;

diff -r 11716a084cae -r 4ba01fea9cfd src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Feb 18 19:18:49 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Feb 18 19:41:25 2018 +0100
@@ -82,7 +82,6 @@
   val amend_registration: string * morphism -> morphism * bool ->
     morphism -> Context.generic -> Context.generic
   val registrations_of: Context.generic -> string -> (string * morphism) list
-  val all_registrations_of: Context.generic -> (string * morphism) list
   val add_dependency: string -> string * morphism -> (morphism * bool) option ->
     morphism -> theory -> theory
 
@@ -393,17 +392,12 @@
     |> compose_mixins
   end;
 
-fun get_registrations context select =
-  Registrations.get context
-  |>> Idtab.dest |>> select
+fun registrations_of context loc =
+  Idtab.fold_rev (fn ((name, _), (reg, _)) => name = loc ? cons (name, reg))
+    (#1 (Registrations.get context)) []
   (* with inherited mixins *)
-  |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
-    (name, base $> (collect_mixins context (name, base $> export)) $> export)) regs);
-
-fun registrations_of context name =
-  get_registrations context (filter (curry (op =) name o fst o fst));
-
-fun all_registrations_of context = get_registrations context I;
+  |> map (fn (name, (base, export)) =>
+      (name, base $> (collect_mixins context (name, base $> export)) $> export));
 
 
 (*** Activate context elements of locale ***)
@@ -601,8 +595,7 @@
         |> (snd o Attrib.global_notes kind
             (Attrib.transform_facts (Morphism.transfer_morphism thy $> morph) facts));
       fun registrations thy =
-        fold_rev (fn (_, morph) => global_notes morph)
-          (registrations_of (Context.Theory thy) loc) thy;
+        fold_rev (global_notes o #2) (registrations_of (Context.Theory thy) loc) thy;
     in
       ctxt
       |> Attrib.local_notes kind facts |> snd