tuned: prefer list operations over Source.source;

--- 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