src/Pure/theory.ML

   include SIGN_THEORY
   val begin_theory: string -> theory list -> theory
   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
   val all_axioms_of: theory -> (string * term) list
   val self_ref: theory -> theory_ref

 fun err_dup_axms dups = error ("Duplicate axiom(s): " ^ commas_quote dups);
 fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
 
 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;
 
   fun extend (Thy {axioms, defs, oracles}) = make_thy (NameSpace.empty_table, defs, oracles);

     in make_thy (axioms, defs, oracles) end;
 
   fun print _ _ = ();
 end);
 
-val init = ThyData.init;
+val init_data = ThyData.init;
 
 fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
 
 fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles}) =>
   make_thy (f (axioms, defs, oracles)));