src/Pure/sign.ML
changeset 4124 1af16493c57f
parent 4052 026069ba0316
child 4140 c62df16811fe
     1.1 --- a/src/Pure/sign.ML	Tue Nov 04 15:16:23 1997 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Nov 04 16:17:04 1997 +0100
     1.3 @@ -110,10 +110,10 @@
     1.4    val add_path: string -> sg -> sg
     1.5    val add_space: string * string list -> sg -> sg
     1.6    val add_name: string -> sg -> sg
     1.7 -  val init_data: string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))
     1.8 -    -> sg -> sg
     1.9 -  val get_data: sg -> string -> exn
    1.10 -  val put_data: string * exn -> sg -> sg
    1.11 +  val init_data: string * (object * (object -> object) *
    1.12 +    (object * object -> object) * (object -> unit)) -> sg -> sg
    1.13 +  val get_data: sg -> string -> object
    1.14 +  val put_data: string * object -> sg -> sg
    1.15    val print_data: sg -> string -> unit
    1.16    val merge_refs: sg_ref * sg_ref -> sg_ref
    1.17    val prep_ext: sg -> sg