--- a/src/Pure/Isar/outer_syntax.ML Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Apr 27 15:06:35 2006 +0200
@@ -197,10 +197,10 @@
|> Source.source T.stopper
(Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME))
(if do_recover then SOME recover else NONE)
- |> Source.mapfilter I
+ |> Source.map_filter I
|> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term do_trace (cmd ())) xs))
(if do_recover then SOME recover else NONE)
- |> Source.mapfilter I
+ |> Source.map_filter I
end;