diff -r 5f9138bcb3d7 -r fb79144af9a3 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/pure_thy.ML	Mon May 07 00:49:59 2007 +0200
@@ -152,7 +152,6 @@
 
 structure TheoremsData = TheoryDataFun
 (struct
-  val name = "Pure/theorems";
   type T =
    {theorems: thm list NameSpace.table,
     index: FactIndex.T} ref;
@@ -505,9 +504,6 @@
 val proto_pure =
   Context.pre_pure_thy
   |> Compress.init_data
-  |> Sign.init_data
-  |> Theory.init_data
-  |> Proofterm.init_data
   |> TheoremsData.init
   |> Sign.add_types
    [("fun", 2, NoSyn),