1.1 --- a/src/Pure/theory.ML	Tue Oct 14 17:34:36 1997 +0200
     1.2 +++ b/src/Pure/theory.ML	Tue Oct 14 17:35:35 1997 +0200
     1.3 @@ -75,6 +75,10 @@
     1.4    val add_path		: string -> theory -> theory
     1.5    val add_space		: string * string list -> theory -> theory
     1.6    val add_name		: string -> theory -> theory
     1.7 +  val init_data		: string * exn * (exn * exn -> exn) * (string -> exn -> Pretty.T)
     1.8 +    -> theory -> theory
     1.9 +  val get_data		: theory -> string -> exn
    1.10 +  val put_data		: string * exn -> theory -> theory
    1.11    val merge_thy_list    : bool -> theory list -> theory
    1.12  end;
    1.13  
    1.14 @@ -375,6 +379,13 @@
    1.15  val add_defs = ext_defns read_axm;
    1.16  
    1.17  
    1.18 +(** additional theory data **)
    1.19 +
    1.20 +val init_data = ext_sg Sign.init_data;
    1.21 +val get_data = Sign.get_data o sign_of;
    1.22 +val put_data = ext_sg Sign.put_data;
    1.23 +
    1.24 +
    1.25  
    1.26  (** merge theories **)
    1.27