# HG changeset patch
# User wenzelm
# Date 878227494 -3600
# Node ID b2a70d318df2d7c25a1c496c74d6402b22d2df8c
# Parent  b9fd385981bd10778205c3046d9f20674ed8d850
tuned thy_data;

diff -r b9fd385981bd -r b2a70d318df2 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Oct 30 17:01:50 1997 +0100
+++ b/src/Pure/pure_thy.ML	Thu Oct 30 17:04:54 1997 +0100
@@ -36,7 +36,7 @@
 
 (** data kind theorems **)
 
-val theorems = "theorems";
+val theoremsK = "theorems";
 
 exception Theorems of
  {space: NameSpace.T,
@@ -69,7 +69,7 @@
 
 in
 
-val theorems_methods = (mk_empty (), mk_empty, mk_empty, print);
+val theorems_data = (theoremsK, (mk_empty (), mk_empty, mk_empty, print));
 
 end;
 
@@ -77,7 +77,7 @@
 (* get data record *)
 
 fun get_theorems_sg sg =
-  (case Sign.get_data sg theorems of
+  (case Sign.get_data sg theoremsK of
     Theorems r => r
   | _ => sys_error "get_theorems_sg");
 
@@ -244,7 +244,7 @@
 
 val proto_pure =
   Theory.pre_pure
-  |> Theory.init_data theorems theorems_methods
+  |> Theory.init_data [theorems_data]
   |> Theory.add_types
    (("fun", 2, NoSyn) ::
     ("prop", 0, NoSyn) ::