src/Pure/Isar/outer_syntax.ML
changeset 19482 9f11af8f7ef9
parent 19060 c814a7856121
child 20023 33124a9f5e31
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -197,10 +197,10 @@
     1.4      |> Source.source T.stopper
     1.5        (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME))
     1.6        (if do_recover then SOME recover else NONE)
     1.7 -    |> Source.mapfilter I
     1.8 +    |> Source.map_filter I
     1.9      |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term do_trace (cmd ())) xs))
    1.10        (if do_recover then SOME recover else NONE)
    1.11 -    |> Source.mapfilter I
    1.12 +    |> Source.map_filter I
    1.13    end;
    1.14  
    1.15