# 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;