src/Pure/defs.ML
changeset 33712 cffc97238102
parent 33701 9dd1079cec3a
child 35845 e5980f0ad025
     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}