diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/theory.ML	Mon May 07 00:49:59 2007 +0200
@@ -21,7 +21,6 @@
   val end_theory: theory -> theory
   val checkpoint: theory -> theory
   val copy: theory -> theory
-  val init_data: theory -> theory
   val rep_theory: theory ->
    {axioms: term NameSpace.table,
     defs: Defs.T,
@@ -101,8 +100,7 @@
 fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
 
 structure ThyData = TheoryDataFun
-(struct
-  val name = "Pure/theory";
+(
   type T = thy;
   val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
   val copy = I;
@@ -119,11 +117,7 @@
       val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
         handle Symtab.DUPS dups => err_dup_oras dups;
     in make_thy (axioms, defs, oracles) end;
-
-  fun print _ _ = ();
-end);
-
-val init_data = ThyData.init;
+);
 
 fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);