src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

   in
     Source.of_string name
     |> Symbol.source
     |> Token.source keywords Position.start
     |> Token.source_proper
-    |> Source.source Token.stopper (Parse.xthms1 >> get)
+    |> Source.source Token.stopper (Parse.thms1 >> get)
     |> Source.exhaust
   end
 
 val one_day = seconds (24.0 * 60.0 * 60.0)
 val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)