src/Pure/theory.ML
changeset 16536 c5744af6b28a
parent 16495 2e99aca906a7
child 16600 55ffcee3b8f3
     1.1 --- a/src/Pure/theory.ML	Wed Jun 22 19:41:20 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Wed Jun 22 19:41:22 2005 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4    val end_theory: theory -> theory
     1.5    val checkpoint: theory -> theory
     1.6    val copy: theory -> theory
     1.7 -  val init: theory -> theory
     1.8 +  val init_data: theory -> theory
     1.9    val axiom_space: theory -> NameSpace.T
    1.10    val oracle_space: theory -> NameSpace.T
    1.11    val axioms_of: theory -> (string * term) list
    1.12 @@ -135,7 +135,7 @@
    1.13  
    1.14  structure ThyData = TheoryDataFun
    1.15  (struct
    1.16 -  val name = "Pure/thy";
    1.17 +  val name = "Pure/theory";
    1.18    type T = thy;
    1.19    val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
    1.20    val copy = I;
    1.21 @@ -158,7 +158,7 @@
    1.22    fun print _ _ = ();
    1.23  end);
    1.24  
    1.25 -val init = ThyData.init;
    1.26 +val init_data = ThyData.init;
    1.27  
    1.28  fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
    1.29