# HG changeset patch
# User wenzelm
# Date 1258375982 -3600
# Node ID cffc97238102d1430dc6f93fd670751c3e745b11
# Parent  2fdb11580b964734a4ba575000f05e4e95898b54
tuned signature;

diff -r 2fdb11580b96 -r cffc97238102 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Mon Nov 16 13:49:21 2009 +0100
+++ b/src/Pure/defs.ML	Mon Nov 16 13:53:02 2009 +0100
@@ -10,10 +10,10 @@
   val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
   val plain_args: typ list -> bool
   type T
-  val all_specifications_of: T -> (string * {def: string option, description: string,
-    lhs: typ list, rhs: (string * typ list) list} list) list
-  val specifications_of: T -> string -> {def: string option, description: string,
-    lhs: typ list, rhs: (string * typ list) list} list
+  type spec =
+    {def: string option, description: string, lhs: typ list, rhs: (string * typ list) list}
+  val all_specifications_of: T -> (string * spec list) list
+  val specifications_of: T -> string -> spec list
   val dest: T ->
    {restricts: ((string * typ list) * string) list,
     reducts: ((string * typ list) * (string * typ list) list) list}