src/Pure/thm.ML
changeset 31947 7daee3bed3af
parent 31945 d5f186aa0bed
child 31977 e03059ae2d82
     1.1 --- a/src/Pure/thm.ML	Mon Jul 06 22:41:00 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Mon Jul 06 22:42:27 2009 +0200
     1.3 @@ -115,6 +115,7 @@
     1.4    val incr_indexes_cterm: int -> cterm -> cterm
     1.5    val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
     1.6    val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
     1.7 +  val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
     1.8    val terms_of_tpairs: (term * term) list -> term list
     1.9    val full_prop_of: thm -> term
    1.10    val maxidx_of: thm -> int
    1.11 @@ -367,6 +368,9 @@
    1.12      prop = cterm maxidx prop}
    1.13    end;
    1.14  
    1.15 +fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
    1.16 +  fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
    1.17 +
    1.18  fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs [];
    1.19  
    1.20  fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';
    1.21 @@ -473,29 +477,28 @@
    1.22  
    1.23  (** sort contexts of theorems **)
    1.24  
    1.25 -fun present_sorts (Thm (_, {hyps, tpairs, prop, ...})) =
    1.26 -  fold (fn (t, u) => Sorts.insert_term t o Sorts.insert_term u) tpairs
    1.27 -    (Sorts.insert_terms hyps (Sorts.insert_term prop []));
    1.28 -
    1.29 -(*remove extra sorts that are non-empty by virtue of type signature information*)
    1.30 +(*remove extra sorts that are witnessed by type signature information*)
    1.31  fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
    1.32    | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
    1.33        let
    1.34          val thy = Theory.deref thy_ref;
    1.35 -        val present = present_sorts thm;
    1.36 -        val extra = Sorts.subtract present shyps;
    1.37 -        val extra' =
    1.38 -          Sorts.subtract (map #2 (Sign.witness_sorts thy present extra)) extra
    1.39 +        val present =
    1.40 +          (fold_terms o fold_types o fold_atyps)
    1.41 +            (fn T as TFree (_, S) => insert (eq_snd op =) (T, S)
    1.42 +              | T as TVar (_, S) => insert (eq_snd op =) (T, S)) thm [];
    1.43 +        val extra = fold (Sorts.remove_sort o #2) present shyps;
    1.44 +        val witnessed = Sign.witness_sorts thy present extra;
    1.45 +        val extra' = fold (Sorts.remove_sort o #2) witnessed extra
    1.46            |> Sorts.minimal_sorts (Sign.classes_of thy);
    1.47 -        val shyps' = Sorts.union present extra'
    1.48 -          |> Sorts.remove_sort [];
    1.49 +        val shyps' = fold (Sorts.insert_sort o #2) present extra';
    1.50        in
    1.51          Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
    1.52            shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
    1.53        end;
    1.54  
    1.55  (*dangling sort constraints of a thm*)
    1.56 -fun extra_shyps (th as Thm (_, {shyps, ...})) = Sorts.subtract (present_sorts th) shyps;
    1.57 +fun extra_shyps (th as Thm (_, {shyps, ...})) =
    1.58 +  Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
    1.59  
    1.60  
    1.61