# HG changeset patch
# User wenzelm
# Date 1247870062 -7200
# Node ID ebb9274e34b74e07051d94e991db1fd38a7d2a47
# Parent  d6065a237059ac1076d263e1649983f24fa8a0b6
tuned;

diff -r d6065a237059 -r ebb9274e34b7 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Sat Jul 18 00:33:57 2009 +0200
+++ b/src/Pure/defs.ML	Sat Jul 18 00:34:22 2009 +0200
@@ -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 * {is_def: bool, name: string,
+    lhs: typ list, rhs: (string * typ list) list} list) list
   val specifications_of: T -> string -> {is_def: bool, name: string,
     lhs: typ list, rhs: (string * typ list) list} list
-  val all_specifications_of: T -> (string * {is_def: bool, name: string,
-    lhs: typ list, rhs: (string * typ list) list} list) list
   val dest: T ->
    {restricts: ((string * typ list) * string) list,
     reducts: ((string * typ list) * (string * typ list) list) list}
@@ -75,9 +75,11 @@
     SOME (def: def) => which def
   | NONE => []);
 
+fun all_specifications_of (Defs defs) =
+  (map o apsnd) (map snd o Inttab.dest o #specs) (Symtab.dest defs);
+
 fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
-fun all_specifications_of (Defs defs) =
-  ((map o apsnd) (map snd o Inttab.dest o #specs) o Symtab.dest) defs;
+
 val restricts_of = lookup_list #restricts;
 val reducts_of = lookup_list #reducts;