tuned message;
authorwenzelm
Tue, 31 Mar 2015 16:43:49 +0200
changeset 59878 05362c246a64
parent 59877 a04ea4709c8d
child 59879 6292f1f5ffae
tuned message;
src/Pure/ML/ml_antiquotations.ML
src/Pure/Tools/named_theorems.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)) #>
 
--- 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;