--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 05 20:05:32 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 05 20:20:57 2014 +0100
@@ -80,7 +80,7 @@
val subgoal_count = Try.subgoal_count
fun reserved_isar_keyword_table () =
- Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
+ Symtab.make_set (Scan.dest_lexicon (Scan.merge_lexicons (Keyword.get_lexicons ())));
exception TOO_MANY of unit
@@ -126,12 +126,11 @@
fun thms_of_name ctxt name =
let
- val lex = Keyword.get_lexicons
val get = maps (Proof_Context.get_fact ctxt o fst)
in
Source.of_string name
|> Symbol.source
- |> Token.source lex Position.start
+ |> Token.source Keyword.get_keywords Position.start
|> Token.source_proper
|> Source.source Token.stopper (Parse.xthms1 >> get)
|> Source.exhaust