src/Pure/Thy/export_theory.ML

--- a/src/Pure/Thy/export_theory.ML	Sat May 06 14:49:54 2023 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sat May 06 23:20:20 2023 +0200
@@ -463,7 +463,7 @@
       let
         val space = get_space thy;
         val export_name = "other/" ^ Name_Space.kind_of space;
-        val decls = Name_Space.decl_names space |> map (rpair ());
+        val decls = Name_Space.get_names space |> map (rpair ());
       in export_entities export_name get_space decls (fn _ => fn () => SOME (K [])) end;
 
     val other_spaces = other_name_spaces thy;