# HG changeset patch # User wenzelm # Date 1148501046 -7200 # Node ID 69c71d40f8a856bc66da17a4aa26d0896d207124 # Parent 3ae3cc4b1eace41ebba6547bd725b2be959cdddf made smlnj happy; diff -r 3ae3cc4b1eac -r 69c71d40f8a8 src/Pure/defs.ML --- a/src/Pure/defs.ML Wed May 24 21:58:09 2006 +0200 +++ b/src/Pure/defs.ML Wed May 24 22:04:06 2006 +0200 @@ -71,7 +71,7 @@ fun lookup_list which defs c = (case Symtab.lookup defs c of - SOME def => which def + SOME (def: def) => which def | NONE => []); fun specifications_of (Defs defs) = lookup_list (Inttab.dest o #specs) defs;