# HG changeset patch
# User wenzelm
# Date 1415216970 -3600
# Node ID f49c4f883c58ba79d0c96644fd6199f00e77dc71
# Parent  38c72f5f6c2e7e8df2596860580a83086581a7cd
eliminated pointless dynamic keywords (TTY legacy);

diff -r 38c72f5f6c2e -r f49c4f883c58 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Nov 05 20:20:57 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Nov 05 20:49:30 2014 +0100
@@ -127,10 +127,11 @@
 fun thms_of_name ctxt name =
   let
     val get = maps (Proof_Context.get_fact ctxt o fst)
+    val keywords = Keyword.get_keywords ()
   in
     Source.of_string name
     |> Symbol.source
-    |> Token.source Keyword.get_keywords Position.start
+    |> Token.source keywords Position.start
     |> Token.source_proper
     |> Source.source Token.stopper (Parse.xthms1 >> get)
     |> Source.exhaust
diff -r 38c72f5f6c2e -r f49c4f883c58 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Nov 05 20:20:57 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Nov 05 20:49:30 2014 +0100
@@ -226,13 +226,13 @@
 fun scan keywords pos =
   Source.of_string #>
   Symbol.source #>
-  Token.source (K keywords) pos #>
+  Token.source keywords pos #>
   Source.exhaust;
 
 fun parse (keywords, syntax) pos str =
   Source.of_string str
   |> Symbol.source
-  |> Token.source (K keywords) pos
+  |> Token.source keywords pos
   |> commands_source syntax
   |> Source.exhaust;
 
diff -r 38c72f5f6c2e -r f49c4f883c58 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Nov 05 20:20:57 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Nov 05 20:49:30 2014 +0100
@@ -79,10 +79,10 @@
   val pretty_src: Proof.context -> src -> Pretty.T
   val ident_or_symbolic: string -> bool
   val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
-  val source: (unit -> Keyword.keywords) ->
+  val source: Keyword.keywords ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
-  val source_strict: (unit -> Keyword.keywords) ->
+  val source_strict: Keyword.keywords ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   type 'a parser = T list -> 'a * T list
@@ -561,14 +561,14 @@
 
 in
 
-fun source' strict get_keywords =
+fun source' strict keywords =
   let
-    val scan_strict = Scan.bulk (fn xs => scan (get_keywords ()) xs);
+    val scan_strict = Scan.bulk (scan keywords);
     val scan = if strict then scan_strict else Scan.recover scan_strict recover;
   in Source.source Symbol_Pos.stopper scan end;
 
-fun source get pos src = Symbol_Pos.source pos src |> source' false get;
-fun source_strict get pos src = Symbol_Pos.source pos src |> source' true get;
+fun source keywords pos src = Symbol_Pos.source pos src |> source' false keywords;
+fun source_strict keywords pos src = Symbol_Pos.source pos src |> source' true keywords;
 
 end;
 
@@ -584,7 +584,7 @@
 
 fun read_no_commands keywords scan syms =
   Source.of_list syms
-  |> source' true (K (Keyword.no_command_keywords keywords))
+  |> source' true (Keyword.no_command_keywords keywords)
   |> source_proper
   |> Source.source stopper (Scan.error (Scan.bulk scan))
   |> Source.exhaust;
diff -r 38c72f5f6c2e -r f49c4f883c58 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Nov 05 20:20:57 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Nov 05 20:49:30 2014 +0100
@@ -147,8 +147,9 @@
   let
     val {name = (name, _), ...} = header;
     val _ = Thy_Header.define_keywords header;
+    val keywords = Keyword.get_keywords ();
 
-    val toks = Outer_Syntax.scan (Keyword.get_keywords ()) text_pos text;
+    val toks = Outer_Syntax.scan keywords text_pos text;
     val spans = Outer_Syntax.parse_spans toks;
     val elements = Thy_Syntax.parse_elements spans;
 
diff -r 38c72f5f6c2e -r f49c4f883c58 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Wed Nov 05 20:20:57 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Wed Nov 05 20:49:30 2014 +0100
@@ -141,7 +141,7 @@
   str
   |> Source.of_string_limited 8000
   |> Symbol.source
-  |> Token.source_strict (K header_keywords) pos;
+  |> Token.source_strict header_keywords pos;
 
 fun read_source pos source =
   let val res =