diff -r a86896359ca4 -r 4263be178c8f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jul 02 21:26:18 2009 +0200
+++ b/src/Pure/thm.ML	Thu Jul 02 22:17:08 2009 +0200
@@ -487,7 +487,8 @@
         val extra' =
           Sorts.subtract (map #2 (Sign.witness_sorts thy present extra)) extra
           |> Sorts.minimal_sorts (Sign.classes_of thy);
-        val shyps' = Sorts.union present extra';
+        val shyps' = Sorts.union present extra'
+          |> Sorts.remove_sort [];
       in
         Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
           shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})