--- a/src/Pure/context.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/context.ML Sun Aug 16 18:19:30 2015 +0200
@@ -34,7 +34,7 @@
type pretty
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
- val theory_name_id: theory_id -> string
+ val theory_id_name: theory_id -> string
val theory_name: theory -> string
val PureN: string
val display_names: theory -> string list
@@ -196,7 +196,7 @@
fun make_history name stage = {name = name, stage = stage};
fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
-val theory_name_id = #name o history_of_id;
+val theory_id_name = #name o history_of_id;
val theory_name = #name o history_of;
val parents_of = #parents o ancestry_of;
val ancestors_of = #ancestors o ancestry_of;