--- 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;