--- a/src/Pure/Thy/thy_header.ML Wed Apr 06 19:50:27 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML Wed Apr 06 23:45:19 2016 +0200
@@ -17,6 +17,9 @@
val add_keywords: keywords -> theory -> theory
val get_keywords: theory -> Keyword.keywords
val get_keywords': Proof.context -> Keyword.keywords
+ val ml_bootstrapN: string
+ val ml_rootN: string
+ val root_mlN: string
val args: header parser
val read: Position.T -> string -> header
val read_tokens: Token.T list -> header
@@ -102,6 +105,13 @@
(** concrete syntax **)
+(* names *)
+
+val ml_bootstrapN = "ML_Bootstrap";
+val ml_rootN = "ML_Root";
+val root_mlN = "ROOT.ML";
+
+
(* header args *)
local