1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Mar 15 23:06:22 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Mar 16 11:26:55 2012 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4  val normalize_chained_theorems =
     1.5    maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
     1.6  fun reserved_isar_keyword_table () =
     1.7 -  union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())
     1.8 +  Keyword.dest () |-> union (op =)
     1.9    |> map (rpair ()) |> Symtab.make
    1.10  
    1.11  end;