tuned errors -- in accordance to ML antiquotations;
authorwenzelm
Fri, 28 Feb 2014 10:50:54 +0100
changeset 55796 be08b88af33d
parent 55795 2d4cf0005a02
child 55797 6a59b4bb7506
tuned errors -- in accordance to ML antiquotations;
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