diff -r 80eb6640f3d5 -r 596fb1eb7856 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Sun Feb 12 20:32:59 2006 +0100
+++ b/src/Pure/defs.ML	Sun Feb 12 21:34:18 2006 +0100
@@ -76,8 +76,8 @@
     val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
       handle Graph.CYCLES cycles => err_cyclic cycles;
     val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
-      SOME (Inttab.fold (fn spec2 => fn specs1 =>
-        (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1));
+      Inttab.fold (fn spec2 => fn specs1 =>
+        (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1);
   in make_defs (consts', specified') end;
 
 end;