author | wenzelm |
Wed, 05 Jun 2024 11:30:26 +0200 | |
changeset 80263 | 8a0ccdcae2d1 |
parent 80262 | d49f3a1c06a6 |
child 80264 | 71c1cf9e7413 |
--- 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;