# HG changeset patch
# User wenzelm
# Date 1503057305 -7200
# Node ID 450cefec7c118095d10856a262e155723f203c9e
# Parent  a8299195ed82cc8a0eb22ff0185106edbfe0676b
more informative error message, e.g. relevant for incoherent imports;

diff -r a8299195ed82 -r 450cefec7c11 src/Pure/context.ML
--- a/src/Pure/context.ML	Thu Aug 17 22:29:30 2017 +0200
+++ b/src/Pure/context.ML	Fri Aug 18 13:55:05 2017 +0200
@@ -165,9 +165,7 @@
 val finished = ~1;
 
 fun display_name thy_id =
-  let
-    val {name = long_name, stage} = history_of_id thy_id;
-    val name = Long_Name.base_name long_name;
+  let val {name, stage} = history_of_id thy_id;
   in if stage = finished then name else name ^ ":" ^ string_of_int stage end;
 
 fun display_names thy =