src/Pure/context.ML

--- a/src/Pure/context.ML	Mon Apr 10 21:05:31 2017 +0200
+++ b/src/Pure/context.ML	Mon Apr 10 21:43:21 2017 +0200
@@ -33,7 +33,9 @@
   val timing: bool Unsynchronized.ref
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
+  val theory_id_long_name: theory_id -> string
   val theory_id_name: theory_id -> string
+  val theory_long_name: theory -> string
   val theory_name: theory -> string
   val PureN: string
   val pretty_thy: theory -> Pretty.T
@@ -148,8 +150,11 @@
 fun make_history name stage = {name = name, stage = stage};
 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
 
-val theory_id_name = #name o history_of_id;
-val theory_name = #name o history_of;
+val theory_id_long_name = #name o history_of_id;
+val theory_id_name = Long_Name.base_name o theory_id_long_name;
+val theory_long_name = #name o history_of;
+val theory_name = Long_Name.base_name o theory_long_name;
+
 val parents_of = #parents o ancestry_of;
 val ancestors_of = #ancestors o ancestry_of;