src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

   in
     Source.of_string name
     |> Symbol.source
     |> Token.source {do_recover = SOME false} lex Position.start
     |> Token.source_proper
-    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
+    |> Source.source Token.stopper (Parse.xthms1 >> get) NONE
     |> 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)