# HG changeset patch
# User wenzelm
# Date 876843335 -7200
# Node ID 0035d1f97096a2b1087f5268fb77aa23581ac4ac
# Parent  e0ce3d4ec47db60691f2429e9c6f77943cb9723a
added init_data, get_data, put_data;

diff -r e0ce3d4ec47d -r 0035d1f97096 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Oct 14 17:34:36 1997 +0200
+++ b/src/Pure/theory.ML	Tue Oct 14 17:35:35 1997 +0200
@@ -75,6 +75,10 @@
   val add_path		: string -> theory -> theory
   val add_space		: string * string list -> theory -> theory
   val add_name		: string -> theory -> theory
+  val init_data		: string * exn * (exn * exn -> exn) * (string -> exn -> Pretty.T)
+    -> theory -> theory
+  val get_data		: theory -> string -> exn
+  val put_data		: string * exn -> theory -> theory
   val merge_thy_list    : bool -> theory list -> theory
 end;
 
@@ -375,6 +379,13 @@
 val add_defs = ext_defns read_axm;
 
 
+(** additional theory data **)
+
+val init_data = ext_sg Sign.init_data;
+val get_data = Sign.get_data o sign_of;
+val put_data = ext_sg Sign.put_data;
+
+
 
 (** merge theories **)