src/Pure/thm.ML
changeset 74112 d0527bb2e590
parent 73860 dfac078e5444
child 74200 17090e27aae9
--- a/src/Pure/thm.ML	Tue Aug 03 12:39:29 2021 +0200
+++ b/src/Pure/thm.ML	Tue Aug 03 13:08:23 2021 +0200
@@ -897,7 +897,7 @@
     unit Name_Space.table *  (*oracles: authentic derivation names*)
     classes;  (*type classes within the logic*)
 
-  val empty : T = (Name_Space.empty_table "oracle", empty_classes);
+  val empty : T = (Name_Space.empty_table Markup.oracleN, empty_classes);
   val extend = I;
   fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T =
     (Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2));