# HG changeset patch
# User haftmann
# Date 1144332464 -7200
# Node ID 59f08f67ed3ffc66c424c394088921d7a2308145
# Parent  952b12ebfdfff533bd42ae6c63705786bff86e81
exported specification names

diff -r 952b12ebfdff -r 59f08f67ed3f src/Pure/defs.ML
--- a/src/Pure/defs.ML	Wed Apr 05 17:38:32 2006 +0200
+++ b/src/Pure/defs.ML	Thu Apr 06 16:07:44 2006 +0200
@@ -12,7 +12,7 @@
   val define: (string -> typ) -> (bool * string) * string
     -> string * typ -> (string * typ) list -> T -> T
   val empty: T
-  val specifications_of: T -> string -> (typ * string) list
+  val specifications_of: T -> string -> (typ * (string * string)) list
   val merge: Pretty.pp -> T * T -> T
 end
 
@@ -71,7 +71,7 @@
 fun specifications_of (Defs {specified, ...}) c =
   (List.mapPartial
     (fn (_, (false, _, _, _)) => NONE
-      | (_, (true, _, thyname, ty)) => SOME (ty, thyname)) o Inttab.dest
+      | (_, (true, specname, thyname, ty)) => SOME (ty, (specname, thyname))) o Inttab.dest
     o the_default Inttab.empty o Symtab.lookup specified) c;