src/Pure/Isar/proof_context.ML
changeset 39441 4110cc1b8f9f
parent 39296 e275d581a218
child 39507 839873937ddd
--- a/src/Pure/Isar/proof_context.ML	Fri Sep 17 17:09:31 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Sep 17 17:10:44 2010 +0200
@@ -734,8 +734,8 @@
 local
 
 fun parse_failed ctxt pos msg kind =
- (Context_Position.report ctxt Markup.bad pos;
-  cat_error msg ("Failed to parse " ^ kind));
+  cat_error msg ("Failed to parse " ^ kind ^
+    Markup.markup Markup.report (Context_Position.reported_text ctxt Markup.bad pos ""));
 
 fun parse_sort ctxt text =
   let