src/Pure/Isar/outer_syntax.ML
changeset 19482 9f11af8f7ef9
parent 19060 c814a7856121
child 20023 33124a9f5e31
--- 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;