--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Nov 06 11:44:41 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Nov 06 13:36:19 2014 +0100
@@ -17,7 +17,6 @@
val parse_bool_option : bool -> string -> string -> bool option
val parse_time : string -> string -> Time.time
val subgoal_count : Proof.state -> int
- val reserved_isar_keyword_table : unit -> unit Symtab.table
val thms_in_proof : int -> (string Symtab.table * string Symtab.table) option -> thm ->
string list option
val thms_of_name : Proof.context -> string -> thm list
@@ -79,9 +78,6 @@
val subgoal_count = Try.subgoal_count
-fun reserved_isar_keyword_table () =
- Symtab.make_set (Scan.dest_lexicon (Scan.merge_lexicons (Keyword.get_lexicons ())));
-
exception TOO_MANY of unit
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to