src/Pure/thm.ML
changeset 31905 4263be178c8f
parent 31903 c5221dbc40f6
child 31943 5e960a0780a2
     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})