# HG changeset patch
# User wenzelm
# Date 1515353556 -3600
# Node ID 408a137e2793989e1e269a8d7ece639a9cf83a33
# Parent  221612c942de51e7334168a16f0b81872bf26cc3
tuned message;

diff -r 221612c942de -r 408a137e2793 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sun Jan 07 16:55:45 2018 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sun Jan 07 20:32:36 2018 +0100
@@ -178,6 +178,7 @@
 open Basic_Symbol_Pos;
 
 val err_prefix = "SML lexical error: ";
+val err_prefix' = "Isabelle/ML lexical error: ";
 
 fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
@@ -299,7 +300,7 @@
   scan_string >> token String ||
   scan_blanks1 >> token Space ||
   Symbol_Pos.scan_comment err_prefix >> token Comment ||
-  Symbol_Pos.scan_comment_cartouche err_prefix >> token Comment_Cartouche ||
+  Symbol_Pos.scan_comment_cartouche err_prefix' >> token Comment_Cartouche ||
   Scan.max token_leq
    (Scan.literal lexicon >> token Keyword)
    (scan_word >> token Word ||