# HG changeset patch
# User wenzelm
# Date 908281475 -7200
# Node ID 1b3e48bdbb931d7de68bd34d0b799936d1003c1f
# Parent  5266f09db46cabd804c88f23e4aa0fda642dd8e8
PRIVATE sig parts;

diff -r 5266f09db46c -r 1b3e48bdbb93 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Oct 13 11:08:28 1998 +0200
+++ b/src/Pure/sign.ML	Tue Oct 13 14:24:35 1998 +0200
@@ -121,11 +121,6 @@
   val add_space: string * string list -> sg -> sg
   val add_name: string -> sg -> sg
   val data_kinds: data -> string list
-  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) *
-    (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
-  val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
-  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
-  val print_data: Object.kind -> sg -> unit
   val merge_refs: sg_ref * sg_ref -> sg_ref
   val merge: sg * sg -> sg
   val prep_ext: sg -> sg
@@ -135,7 +130,17 @@
   val class_of_const: string -> class
 end;
 
-structure Sign: SIGN =
+signature SIGN_PRIVATE =
+sig
+  include SIGN
+  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) *
+    (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
+  val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
+  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
+  val print_data: Object.kind -> sg -> unit
+end;
+
+structure Sign: SIGN_PRIVATE =
 struct
 
 
diff -r 5266f09db46c -r 1b3e48bdbb93 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Oct 13 11:08:28 1998 +0200
+++ b/src/Pure/theory.ML	Tue Oct 13 14:24:35 1998 +0200
@@ -79,19 +79,24 @@
   val root_path: theory -> theory
   val add_space: string * string list -> theory -> theory
   val add_name: string -> theory -> theory
-  val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) *
-    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
-  val print_data: Object.kind -> theory -> unit
-  val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
-  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
   val prep_ext: theory -> theory
   val prep_ext_merge: theory list -> theory
   val requires: theory -> string -> string -> unit
   val pre_pure: theory
 end;
 
+signature THEORY_PRIVATE =
+sig
+  include THEORY
+  val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) *
+    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
+  val print_data: Object.kind -> theory -> unit
+  val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
+  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
+end;
 
-structure Theory: THEORY =
+
+structure Theory: THEORY_PRIVATE =
 struct
 
 
diff -r 5266f09db46c -r 1b3e48bdbb93 src/Pure/theory_data.ML
--- a/src/Pure/theory_data.ML	Tue Oct 13 11:08:28 1998 +0200
+++ b/src/Pure/theory_data.ML	Tue Oct 13 14:24:35 1998 +0200
@@ -47,3 +47,9 @@
 val put = Theory.put_data kind Data;
 
 end;
+
+(* FIXME deactivated due to Provers/classical.ML legacy code
+(*hide private data access functions*)
+structure Sign: SIGN = Sign;
+structure Theory: THEORY = Theory;
+*)