# HG changeset patch
# User wenzelm
# Date 1393581054 -3600
# Node ID be08b88af33dd25542dde52a739a76c58d3862e7
# Parent  2d4cf0005a02741db7b3880e9394b855eacc366d
tuned errors -- in accordance to ML antiquotations;

diff -r 2d4cf0005a02 -r be08b88af33d src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Feb 28 10:40:04 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Feb 28 10:50:54 2014 +0100
@@ -96,11 +96,7 @@
     val ((xname, _), pos) = Args.dest_src src;
     val (name, f) =
       Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) (xname, pos);
-  in
-    f src state ctxt handle ERROR msg =>
-      cat_error msg ("The error(s) above occurred in document antiquotation: " ^
-        quote name ^ Position.here pos)
-  end;
+  in f src state ctxt end;
 
 fun option ((xname, pos), s) ctxt =
   let