--- 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 ();