--- a/src/Pure/Thy/thy_header.ML Sat Apr 09 19:09:11 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML Sat Apr 09 19:30:15 2016 +0200
@@ -18,8 +18,7 @@
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 ml_roots: string list
val args: header parser
val read: Position.T -> string -> header
val read_tokens: Token.T list -> header
@@ -108,8 +107,8 @@
(* names *)
val ml_bootstrapN = "ML_Bootstrap";
-val ml_rootN = "ML_Root";
-val root_mlN = "ROOT.ML";
+val ml_roots = ["ML_Root0", "ML_Root"];
+
(* header args *)