| changeset 80263 | 8a0ccdcae2d1 |
| parent 80074 | 951c371c1cd9 |
| child 80295 | 8a9588ffc133 |
--- 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;