# HG changeset patch
# User wenzelm
# Date 1331927147 -3600
# Node ID 38aaa08fb37f52acfb2dd69251ebcf29ad186428
# Parent  499d9bbd8de9a41e460435411163be5405cde616
less redundant data;

diff -r 499d9bbd8de9 -r 38aaa08fb37f src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Fri Mar 16 20:33:33 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Fri Mar 16 20:45:47 2012 +0100
@@ -30,7 +30,7 @@
   val prf_asm: T
   val prf_asm_goal: T
   val prf_script: T
-  val kinds: string list
+  val kinds: T list
   val tag: string -> T -> T
   val tags_of: T -> string list
   val tag_theory: T -> T
@@ -100,8 +100,7 @@
 val kinds =
   [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
     thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
-    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
- |> map kind_of;
+    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
 
 
 (* tags *)
@@ -116,29 +115,7 @@
 
 (* external names *)
 
-val name_table = Symtab.make
-  [("control",            control),
-   ("diag",               diag),
-   ("thy_begin",          thy_begin),
-   ("thy_end",            thy_end),
-   ("thy_heading",        thy_heading),
-   ("thy_decl",           thy_decl),
-   ("thy_script",         thy_script),
-   ("thy_goal",           thy_goal),
-   ("thy_schematic_goal", thy_schematic_goal),
-   ("qed",                qed),
-   ("qed_block",          qed_block),
-   ("qed_global",         qed_global),
-   ("prf_heading",        prf_heading),
-   ("prf_goal",           prf_goal),
-   ("prf_block",          prf_block),
-   ("prf_open",           prf_open),
-   ("prf_close",          prf_close),
-   ("prf_chain",          prf_chain),
-   ("prf_decl",           prf_decl),
-   ("prf_asm",            prf_asm),
-   ("prf_asm_goal",       prf_asm_goal),
-   ("prf_script",         prf_script)];
+val name_table = Symtab.make (map (`kind_of) kinds);
 
 type spec = string * string list;
 
diff -r 499d9bbd8de9 -r 38aaa08fb37f src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Fri Mar 16 20:33:33 2012 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Fri Mar 16 20:45:47 2012 +0100
@@ -76,7 +76,7 @@
   |> command Keyword.prf_asm_goal     goal
   |> command Keyword.prf_script       proofstep;
 
-val _ = subset (op =) (Keyword.kinds, Symtab.keys command_keywords)
+val _ = subset (op =) (map Keyword.kind_of Keyword.kinds, Symtab.keys command_keywords)
   orelse raise Fail "Incomplete coverage of command keywords";
 
 fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]