src/Pure/defs.ML
changeset 19339 59f08f67ed3f
parent 19135 2de31ba562d7
child 19482 9f11af8f7ef9
     1.1 --- a/src/Pure/defs.ML	Wed Apr 05 17:38:32 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Apr 06 16:07:44 2006 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    val define: (string -> typ) -> (bool * string) * string
     1.5      -> string * typ -> (string * typ) list -> T -> T
     1.6    val empty: T
     1.7 -  val specifications_of: T -> string -> (typ * string) list
     1.8 +  val specifications_of: T -> string -> (typ * (string * string)) list
     1.9    val merge: Pretty.pp -> T * T -> T
    1.10  end
    1.11  
    1.12 @@ -71,7 +71,7 @@
    1.13  fun specifications_of (Defs {specified, ...}) c =
    1.14    (List.mapPartial
    1.15      (fn (_, (false, _, _, _)) => NONE
    1.16 -      | (_, (true, _, thyname, ty)) => SOME (ty, thyname)) o Inttab.dest
    1.17 +      | (_, (true, specname, thyname, ty)) => SOME (ty, (specname, thyname))) o Inttab.dest
    1.18      o the_default Inttab.empty o Symtab.lookup specified) c;
    1.19  
    1.20