--- a/src/Pure/Isar/keyword.ML Thu Aug 23 12:00:11 2012 +0200
+++ b/src/Pure/Isar/keyword.ML Thu Aug 23 12:33:42 2012 +0200
@@ -57,7 +57,6 @@
val command_tags: string -> string list
val dest: unit -> string list * string list
val status: unit -> unit
- val thy_load_commands: keywords -> (string * string list) list
val define_keywords: string * T option -> keywords -> keywords
val define: string * T option -> unit
val is_diag: string -> bool
@@ -221,11 +220,6 @@
in () end;
-fun thy_load_commands (Keywords {commands, ...}) =
- Symtab.fold (fn (name, Keyword {kind, files, ...}) =>
- kind = kind_of thy_load ? cons (name, files)) commands [];
-
-
(* define *)
fun define_keywords (name, opt_kind) = map_keywords (fn ((minor, major), commands) =>