src/Pure/Isar/locale.ML
changeset 69056 bc4cc763b0ea
parent 69055 dab89758545c
child 69057 56c6378ebaea
--- a/src/Pure/Isar/locale.ML	Mon Sep 24 15:34:19 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Sep 24 19:06:56 2018 +0200
@@ -420,13 +420,6 @@
     |> compose_mixins
   end;
 
-fun registrations_of context loc =
-  Idtab.fold_rev (fn ((name, _), {morphisms, ...}) =>
-    name = loc ? cons (name, morphisms)) (get_regs context) []
-  (* with inherited mixins *)
-  |> map (fn (name, (base, export)) =>
-      (name, base $> (collect_mixins context (name, base $> export)) $> export));
-
 
 (*** Activate context elements of locale ***)
 
@@ -605,6 +598,13 @@
 
 (*** Dependencies ***)
 
+fun registrations_of context loc =
+  Idtab.fold_rev (fn ((name, _), {morphisms, ...}) =>
+    name = loc ? cons (name, morphisms)) (get_regs context) []
+  (*with inherited mixins*)
+  |> map (fn (name, (base, export)) =>
+      (name, base $> (collect_mixins context (name, base $> export)) $> export));
+
 fun add_dependency loc {dep = (name, morph), mixin, export} thy =
   let
     val serial' = serial ();