# HG changeset patch
# User wenzelm
# Date 1246565828 -7200
# Node ID 4263be178c8f057ae1a5a1d33489e711966ff31a
# Parent  a86896359ca4d6f60d3339474e28f3c7f7adc2fc
strip_shyps: remove top sort, which is logically insignificant;

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})