src/Pure/context.ML
changeset 66452 450cefec7c11
parent 65460 fe4cf0de13cb
child 67621 8f93d878f855
equal deleted inserted replaced
66450:a8299195ed82 66452:450cefec7c11
   163 
   163 
   164 val PureN = "Pure";
   164 val PureN = "Pure";
   165 val finished = ~1;
   165 val finished = ~1;
   166 
   166 
   167 fun display_name thy_id =
   167 fun display_name thy_id =
   168   let
   168   let val {name, stage} = history_of_id thy_id;
   169     val {name = long_name, stage} = history_of_id thy_id;
       
   170     val name = Long_Name.base_name long_name;
       
   171   in if stage = finished then name else name ^ ":" ^ string_of_int stage end;
   169   in if stage = finished then name else name ^ ":" ^ string_of_int stage end;
   172 
   170 
   173 fun display_names thy =
   171 fun display_names thy =
   174   let
   172   let
   175     val name = display_name (theory_id thy);
   173     val name = display_name (theory_id thy);