--- a/src/Pure/Thy/thy_header.ML Tue Aug 21 16:56:18 2012 +0200
+++ b/src/Pure/Thy/thy_header.ML Tue Aug 21 20:32:33 2012 +0200
@@ -6,13 +6,13 @@
signature THY_HEADER =
sig
+ type keywords = (string * Keyword.spec option) list
type header =
{name: string,
imports: string list,
- keywords: (string * Keyword.spec option) list,
+ keywords: keywords,
uses: (Path.T * bool) list}
- val make: string -> string list -> (string * Keyword.spec option) list ->
- (Path.T * bool) list -> header
+ val make: string -> string list -> keywords -> (Path.T * bool) list -> header
val define_keywords: header -> unit
val declare_keyword: string * Keyword.spec option -> theory -> theory
val the_keyword: theory -> string -> Keyword.spec option
@@ -23,10 +23,12 @@
structure Thy_Header: THY_HEADER =
struct
+type keywords = (string * Keyword.spec option) list;
+
type header =
{name: string,
imports: string list,
- keywords: (string * Keyword.spec option) list,
+ keywords: keywords,
uses: (Path.T * bool) list};
fun make name imports keywords uses : header =