# HG changeset patch
# User wenzelm
# Date 1516816445 -3600
# Node ID 88a02f41246a9d7b78a15386a855dd21091f9256
# Parent  3a0b08e7dfe9da706be72960da2d85cfb9f6df5f
tuned: prefer list operations over Source.source;

diff -r 3a0b08e7dfe9 -r 88a02f41246a src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jan 24 16:34:24 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jan 24 18:54:05 2018 +0100
@@ -126,10 +126,10 @@
     val get = maps (Proof_Context.get_fact ctxt o fst)
     val keywords = Thy_Header.get_keywords' ctxt
   in
-    Symbol.explode name
+    Symbol_Pos.explode (name, Position.start)
+    |> Token.tokenize keywords {strict = false}
+    |> filter Token.is_proper
     |> Source.of_list
-    |> Token.source keywords Position.start
-    |> Token.source_proper
     |> Source.source Token.stopper (Parse.thms1 >> get)
     |> Source.exhaust
   end