src/Pure/context.ML
changeset 60948 b710a5087116
parent 60947 d5f7b424ba47
child 61044 b7af255dd200
--- 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;