tuned errors -- in accordance to ML antiquotations;
authorwenzelm
Fri, 28 Feb 2014 10:50:54 +0100
changeset 57138be08b88af33d
parent 57137 2d4cf0005a02
child 57139 6a59b4bb7506
tuned errors -- in accordance to ML antiquotations;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Fri Feb 28 10:40:04 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Feb 28 10:50:54 2014 +0100
     1.3 @@ -96,11 +96,7 @@
     1.4      val ((xname, _), pos) = Args.dest_src src;
     1.5      val (name, f) =
     1.6        Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) (xname, pos);
     1.7 -  in
     1.8 -    f src state ctxt handle ERROR msg =>
     1.9 -      cat_error msg ("The error(s) above occurred in document antiquotation: " ^
    1.10 -        quote name ^ Position.here pos)
    1.11 -  end;
    1.12 +  in f src state ctxt end;
    1.13  
    1.14  fun option ((xname, pos), s) ctxt =
    1.15    let