--- a/src/Pure/Thy/thy_header.ML Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML Thu Nov 06 11:44:41 2014 +0100
@@ -12,7 +12,7 @@
imports: (string * Position.T) list,
keywords: keywords}
val make: string * Position.T -> (string * Position.T) list -> keywords -> header
- val define_keywords: header -> unit
+ val define_keywords: keywords -> unit
val declare_keyword: string * Keyword.spec option -> theory -> theory
val the_keyword: theory -> string -> Keyword.spec option
val args: header parser
@@ -37,7 +37,7 @@
(** keyword declarations **)
-fun define_keywords ({keywords, ...}: header) =
+fun define_keywords (keywords: keywords) =
List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);