src/Pure/theory.ML
changeset 22846 fb79144af9a3
parent 22697 92f8e9a8df78
child 23086 12320f6e2523
     1.1 --- a/src/Pure/theory.ML	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -21,7 +21,6 @@
     1.4    val end_theory: theory -> theory
     1.5    val checkpoint: theory -> theory
     1.6    val copy: theory -> theory
     1.7 -  val init_data: theory -> theory
     1.8    val rep_theory: theory ->
     1.9     {axioms: term NameSpace.table,
    1.10      defs: Defs.T,
    1.11 @@ -101,8 +100,7 @@
    1.12  fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
    1.13  
    1.14  structure ThyData = TheoryDataFun
    1.15 -(struct
    1.16 -  val name = "Pure/theory";
    1.17 +(
    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 @@ -119,11 +117,7 @@
    1.22        val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
    1.23          handle Symtab.DUPS dups => err_dup_oras dups;
    1.24      in make_thy (axioms, defs, oracles) end;
    1.25 -
    1.26 -  fun print _ _ = ();
    1.27 -end);
    1.28 -
    1.29 -val init_data = ThyData.init;
    1.30 +);
    1.31  
    1.32  fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
    1.33