src/Pure/ML/ml_antiquotations.ML
changeset 59878 05362c246a64
parent 59812 675d0c692c41
child 59934 b65c4370f831
--- a/src/Pure/ML/ml_antiquotations.ML	Tue Mar 31 15:29:09 2015 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Tue Mar 31 16:43:49 2015 +0200
@@ -47,7 +47,7 @@
                     |> filter completed
                     |> map (fn a => (a, ("system_option", a))));
               val report = Markup.markup_report (Completion.reported_text completion);
-            in cat_error msg report end;
+            in error (msg ^ report) end;
         val _ = Context_Position.report ctxt pos markup;
       in ML_Syntax.print_string name end)) #>