tuned signature;
authorwenzelm
Mon Nov 16 13:53:02 2009 +0100 (2009-11-16)
changeset 33712cffc97238102
parent 33711 2fdb11580b96
child 33713 5249bbca5fab
tuned signature;
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Mon Nov 16 13:49:21 2009 +0100
     1.2 +++ b/src/Pure/defs.ML	Mon Nov 16 13:53:02 2009 +0100
     1.3 @@ -10,10 +10,10 @@
     1.4    val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
     1.5    val plain_args: typ list -> bool
     1.6    type T
     1.7 -  val all_specifications_of: T -> (string * {def: string option, description: string,
     1.8 -    lhs: typ list, rhs: (string * typ list) list} list) list
     1.9 -  val specifications_of: T -> string -> {def: string option, description: string,
    1.10 -    lhs: typ list, rhs: (string * typ list) list} list
    1.11 +  type spec =
    1.12 +    {def: string option, description: string, lhs: typ list, rhs: (string * typ list) list}
    1.13 +  val all_specifications_of: T -> (string * spec list) list
    1.14 +  val specifications_of: T -> string -> spec list
    1.15    val dest: T ->
    1.16     {restricts: ((string * typ list) * string) list,
    1.17      reducts: ((string * typ list) * (string * typ list) list) list}