src/Pure/sign.ML
changeset 5642 1b3e48bdbb93
parent 5635 b7d6b7f66131
child 6040 bd37dc0f56d9
     1.1 --- a/src/Pure/sign.ML	Tue Oct 13 11:08:28 1998 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Oct 13 14:24:35 1998 +0200
     1.3 @@ -121,11 +121,6 @@
     1.4    val add_space: string * string list -> sg -> sg
     1.5    val add_name: string -> sg -> sg
     1.6    val data_kinds: data -> string list
     1.7 -  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) *
     1.8 -    (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
     1.9 -  val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
    1.10 -  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
    1.11 -  val print_data: Object.kind -> sg -> unit
    1.12    val merge_refs: sg_ref * sg_ref -> sg_ref
    1.13    val merge: sg * sg -> sg
    1.14    val prep_ext: sg -> sg
    1.15 @@ -135,7 +130,17 @@
    1.16    val class_of_const: string -> class
    1.17  end;
    1.18  
    1.19 -structure Sign: SIGN =
    1.20 +signature SIGN_PRIVATE =
    1.21 +sig
    1.22 +  include SIGN
    1.23 +  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) *
    1.24 +    (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
    1.25 +  val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
    1.26 +  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
    1.27 +  val print_data: Object.kind -> sg -> unit
    1.28 +end;
    1.29 +
    1.30 +structure Sign: SIGN_PRIVATE =
    1.31  struct
    1.32  
    1.33