src/Pure/Syntax/scan.ML
changeset 5048 2af6b01e7ab6
parent 4968 c68a9c510c90
child 5861 7536314d9a5f
--- a/src/Pure/Syntax/scan.ML	Thu Jun 18 10:52:34 1998 +0200
+++ b/src/Pure/Syntax/scan.ML	Thu Jun 18 11:20:54 1998 +0200
@@ -193,7 +193,7 @@
 
     fun drain_loop recover inp =
       drain_with (catch scanner) inp handle FAIL msg =>
-        (warning (if_none msg "Syntax error."); warning "Trying to recover ...";
+        (error_msg (if_none msg "Syntax error."); error_msg "Trying to recover ...";
           drain_loop recover (apfst snd (drain_with recover inp)));
 
     val ((ys, (state', xs')), src') =