strip_shyps: remove top sort, which is logically insignificant;
authorwenzelm
Thu Jul 02 22:17:08 2009 +0200 (2009-07-02)
changeset 319054263be178c8f
parent 31904 a86896359ca4
child 31917 342a0bad5adf
strip_shyps: remove top sort, which is logically insignificant;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Thu Jul 02 21:26:18 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Jul 02 22:17:08 2009 +0200
     1.3 @@ -487,7 +487,8 @@
     1.4          val extra' =
     1.5            Sorts.subtract (map #2 (Sign.witness_sorts thy present extra)) extra
     1.6            |> Sorts.minimal_sorts (Sign.classes_of thy);
     1.7 -        val shyps' = Sorts.union present extra';
     1.8 +        val shyps' = Sorts.union present extra'
     1.9 +          |> Sorts.remove_sort [];
    1.10        in
    1.11          Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
    1.12            shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})