# HG changeset patch
# User wenzelm
# Date 1427813029 -7200
# Node ID 05362c246a6491c337b35725a424a491e1842d28
# Parent  a04ea4709c8df61289a837a81077a3d71605113e
tuned message;

diff -r a04ea4709c8d -r 05362c246a64 src/Pure/ML/ml_antiquotations.ML
--- 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)) #>
 
diff -r a04ea4709c8d -r 05362c246a64 src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Tue Mar 31 15:29:09 2015 +0200
+++ b/src/Pure/Tools/named_theorems.ML	Tue Mar 31 16:43:49 2015 +0200
@@ -86,7 +86,7 @@
       let
         val thy = Proof_Context.theory_of ctxt;
         val name = Global_Theory.check_fact thy (xname, pos);
-        val _ = get ctxt name handle ERROR msg => cat_error msg (Position.here pos);
+        val _ = get ctxt name handle ERROR msg => error (msg ^ Position.here pos);
       in ML_Syntax.print_string name end)));
 
 end;