equal
deleted
inserted
replaced
333 val lex = OuterKeyword.get_lexicons |
333 val lex = OuterKeyword.get_lexicons |
334 val get = maps (ProofContext.get_fact ctxt o fst) |
334 val get = maps (ProofContext.get_fact ctxt o fst) |
335 in |
335 in |
336 Source.of_string name |
336 Source.of_string name |
337 |> Symbol.source {do_recover=false} |
337 |> Symbol.source {do_recover=false} |
338 |> OuterLex.source {do_recover=SOME false} lex Position.start |
338 |> Token.source {do_recover=SOME false} lex Position.start |
339 |> OuterLex.source_proper |
339 |> Token.source_proper |
340 |> Source.source OuterLex.stopper (Parse_Spec.xthms1 >> get) NONE |
340 |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE |
341 |> Source.exhaust |
341 |> Source.exhaust |
342 end |
342 end |
343 |
343 |
344 in |
344 in |
345 |
345 |