changeset 58028 | e4250d370657 |
parent 57882 | 38bf4de248a6 |
child 58634 | 9f10d82e8188 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Aug 21 13:46:29 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Aug 21 22:48:39 2014 +0200 @@ -136,7 +136,7 @@ |> 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