added Term.fold_atyps_sorts convenience;
authorwenzelm
Sat Mar 27 15:47:57 2010 +0100 (2010-03-27)
changeset 35986b7fcca3d9a44
parent 35985 0bbf0d2348f9
child 35987 7c728daf4876
added Term.fold_atyps_sorts convenience;
src/Pure/term.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/term.ML	Sat Mar 27 15:20:31 2010 +0100
     1.2 +++ b/src/Pure/term.ML	Sat Mar 27 15:47:57 2010 +0100
     1.3 @@ -72,6 +72,7 @@
     1.4    val map_type_tfree: (string * sort -> typ) -> typ -> typ
     1.5    val map_types: (typ -> typ) -> term -> term
     1.6    val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
     1.7 +  val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
     1.8    val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
     1.9    val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.10    val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.11 @@ -431,6 +432,9 @@
    1.12  fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
    1.13    | fold_atyps f T = f T;
    1.14  
    1.15 +fun fold_atyps_sorts f =
    1.16 +  fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S));
    1.17 +
    1.18  fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
    1.19    | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
    1.20    | fold_aterms f a = f a;
     2.1 --- a/src/Pure/thm.ML	Sat Mar 27 15:20:31 2010 +0100
     2.2 +++ b/src/Pure/thm.ML	Sat Mar 27 15:47:57 2010 +0100
     2.3 @@ -484,10 +484,7 @@
     2.4    | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
     2.5        let
     2.6          val thy = Theory.deref thy_ref;
     2.7 -        val present =
     2.8 -          (fold_terms o fold_types o fold_atyps)
     2.9 -            (fn T as TFree (_, S) => insert (eq_snd op =) (T, S)
    2.10 -              | T as TVar (_, S) => insert (eq_snd op =) (T, S)) thm [];
    2.11 +        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
    2.12          val extra = fold (Sorts.remove_sort o #2) present shyps;
    2.13          val witnessed = Sign.witness_sorts thy present extra;
    2.14          val extra' = fold (Sorts.remove_sort o #2) witnessed extra