more informative error message, e.g. relevant for incoherent imports;
authorwenzelm
Fri Aug 18 13:55:05 2017 +0200 (22 months ago)
changeset 66452450cefec7c11
parent 66450 a8299195ed82
child 66453 cc19f7ca2ed6
more informative error message, e.g. relevant for incoherent imports;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Thu Aug 17 22:29:30 2017 +0200
     1.2 +++ b/src/Pure/context.ML	Fri Aug 18 13:55:05 2017 +0200
     1.3 @@ -165,9 +165,7 @@
     1.4  val finished = ~1;
     1.5  
     1.6  fun display_name thy_id =
     1.7 -  let
     1.8 -    val {name = long_name, stage} = history_of_id thy_id;
     1.9 -    val name = Long_Name.base_name long_name;
    1.10 +  let val {name, stage} = history_of_id thy_id;
    1.11    in if stage = finished then name else name ^ ":" ^ string_of_int stage end;
    1.12  
    1.13  fun display_names thy =