# HG changeset patch
# User wenzelm
# Date 1537808816 -7200
# Node ID bc4cc763b0eab39ff0dcaad56af433f3ccd5a070
# Parent  dab89758545cc3c99871b7d8fff39bddb1d3c955
tuned (according to signature);

diff -r dab89758545c -r bc4cc763b0ea src/Pure/Isar/locale.ML
--- 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 ();