src/Pure/Thy/export_theory.ML
changeset 77970 31ea5c1f874d
parent 77889 5db014c36f42
child 77979 a12c48fbf10f
--- a/src/Pure/Thy/export_theory.ML	Fri May 05 12:34:23 2023 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri May 05 15:56:12 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.get_names space |> map (rpair ());
+        val decls = Name_Space.decl_names space |> map (rpair ());
       in export_entities export_name get_space decls (fn _ => fn () => SOME (K [])) end;
 
     val other_spaces = other_name_spaces thy;