added init_data, get_data, put_data;
authorwenzelm
Tue, 14 Oct 1997 17:35:35 +0200
changeset 3865 0035d1f97096
parent 3864 e0ce3d4ec47d
child 3866 97f66ba17458
added init_data, get_data, put_data;
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 **)