# HG changeset patch
# User wenzelm
# Date 1717579826 -7200
# Node ID 8a0ccdcae2d168365809a4be3885b3dfe3db3b19
# Parent  d49f3a1c06a65b924855d853c80d7845200664f4
remove unused (see also 04214caeb9ac);

diff -r d49f3a1c06a6 -r 8a0ccdcae2d1 src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Tue Jun 04 15:13:26 2024 +0200
+++ b/src/Pure/Build/export_theory.ML	Wed Jun 05 11:30:26 2024 +0200
@@ -16,8 +16,6 @@
 
 (* other name spaces *)
 
-fun err_dup_kind kind = error ("Duplicate name space kind " ^ quote kind);
-
 structure Data = Theory_Data
 (
   type T = (theory -> Name_Space.T) Inttab.table;