more informative error message, e.g. relevant for incoherent imports;
--- 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 =