--- a/src/Pure/theory.ML Wed Jun 22 19:41:20 2005 +0200
+++ b/src/Pure/theory.ML Wed Jun 22 19:41:22 2005 +0200
@@ -33,7 +33,7 @@
val end_theory: theory -> theory
val checkpoint: theory -> theory
val copy: theory -> theory
- val init: theory -> theory
+ val init_data: theory -> theory
val axiom_space: theory -> NameSpace.T
val oracle_space: theory -> NameSpace.T
val axioms_of: theory -> (string * term) list
@@ -135,7 +135,7 @@
structure ThyData = TheoryDataFun
(struct
- val name = "Pure/thy";
+ val name = "Pure/theory";
type T = thy;
val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
val copy = I;
@@ -158,7 +158,7 @@
fun print _ _ = ();
end);
-val init = ThyData.init;
+val init_data = ThyData.init;
fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);