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