src/Pure/thm.ML
changeset 35986 b7fcca3d9a44
parent 35854 d452abc96459
child 36330 0584e203960e
     1.1 --- a/src/Pure/thm.ML	Sat Mar 27 15:20:31 2010 +0100
     1.2 +++ b/src/Pure/thm.ML	Sat Mar 27 15:47:57 2010 +0100
     1.3 @@ -484,10 +484,7 @@
     1.4    | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
     1.5        let
     1.6          val thy = Theory.deref thy_ref;
     1.7 -        val present =
     1.8 -          (fold_terms o fold_types o fold_atyps)
     1.9 -            (fn T as TFree (_, S) => insert (eq_snd op =) (T, S)
    1.10 -              | T as TVar (_, S) => insert (eq_snd op =) (T, S)) thm [];
    1.11 +        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
    1.12          val extra = fold (Sorts.remove_sort o #2) present shyps;
    1.13          val witnessed = Sign.witness_sorts thy present extra;
    1.14          val extra' = fold (Sorts.remove_sort o #2) witnessed extra