src/Pure/theory.ML

 fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
 
 structure ThyData = TheoryDataFun
 (
   type T = thy;
-  val empty_axioms = Name_Space.empty_table "axiom";
+  val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
   val empty = make_thy (empty_axioms, Defs.empty, ([], []));
   val copy = I;
 
   fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);