1.1 --- a/src/Pure/Isar/keyword.ML	Fri Mar 16 20:33:33 2012 +0100
     1.2 +++ b/src/Pure/Isar/keyword.ML	Fri Mar 16 20:45:47 2012 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4    val prf_asm: T
     1.5    val prf_asm_goal: T
     1.6    val prf_script: T
     1.7 -  val kinds: string list
     1.8 +  val kinds: T list
     1.9    val tag: string -> T -> T
    1.10    val tags_of: T -> string list
    1.11    val tag_theory: T -> T
    1.12 @@ -100,8 +100,7 @@
    1.13  val kinds =
    1.14    [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
    1.15      thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
    1.16 -    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
    1.17 - |> map kind_of;
    1.18 +    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    1.19  
    1.20  
    1.21  (* tags *)
    1.22 @@ -116,29 +115,7 @@
    1.23  
    1.24  (* external names *)
    1.25  
    1.26 -val name_table = Symtab.make
    1.27 -  [("control",            control),
    1.28 -   ("diag",               diag),
    1.29 -   ("thy_begin",          thy_begin),
    1.30 -   ("thy_end",            thy_end),
    1.31 -   ("thy_heading",        thy_heading),
    1.32 -   ("thy_decl",           thy_decl),
    1.33 -   ("thy_script",         thy_script),
    1.34 -   ("thy_goal",           thy_goal),
    1.35 -   ("thy_schematic_goal", thy_schematic_goal),
    1.36 -   ("qed",                qed),
    1.37 -   ("qed_block",          qed_block),
    1.38 -   ("qed_global",         qed_global),
    1.39 -   ("prf_heading",        prf_heading),
    1.40 -   ("prf_goal",           prf_goal),
    1.41 -   ("prf_block",          prf_block),
    1.42 -   ("prf_open",           prf_open),
    1.43 -   ("prf_close",          prf_close),
    1.44 -   ("prf_chain",          prf_chain),
    1.45 -   ("prf_decl",           prf_decl),
    1.46 -   ("prf_asm",            prf_asm),
    1.47 -   ("prf_asm_goal",       prf_asm_goal),
    1.48 -   ("prf_script",         prf_script)];
    1.49 +val name_table = Symtab.make (map (`kind_of) kinds);
    1.50  
    1.51  type spec = string * string list;
    1.52  

     2.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Fri Mar 16 20:33:33 2012 +0100
     2.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Fri Mar 16 20:45:47 2012 +0100
     2.3 @@ -76,7 +76,7 @@
     2.4    |> command Keyword.prf_asm_goal     goal
     2.5    |> command Keyword.prf_script       proofstep;
     2.6  
     2.7 -val _ = subset (op =) (Keyword.kinds, Symtab.keys command_keywords)
     2.8 +val _ = subset (op =) (map Keyword.kind_of Keyword.kinds, Symtab.keys command_keywords)
     2.9    orelse raise Fail "Incomplete coverage of command keywords";
    2.10  
    2.11  fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]