--- 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 **)