# HG changeset patch
# User wenzelm
# Date 1140035700 -3600
# Node ID 527bc006f2b6888e30df441f0b91b41b351503d1
# Parent  2103a8e14eaa4b0bae0ac0bef634a83d1a555378
specifications_of: avoid partiality;

diff -r 2103a8e14eaa -r 527bc006f2b6 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Wed Feb 15 21:34:59 2006 +0100
+++ b/src/Pure/defs.ML	Wed Feb 15 21:35:00 2006 +0100
@@ -65,8 +65,9 @@
         (check_specified c spec specs; Inttab.update spec specs));
   in (consts', specified') end);
 
-fun specifications_of (Defs { specified, ... }) c =
-  (map (snd o snd) o Inttab.dest o the o Symtab.lookup specified) c;
+fun specifications_of (Defs {specified, ...}) c =
+  (map (snd o snd) o Inttab.dest o the_default Inttab.empty o Symtab.lookup specified) c;
+
 
 (* empty and merge *)