# HG changeset patch
# User wenzelm
# Date 1269701277 -3600
# Node ID b7fcca3d9a441af04c807d547fbc59f42811e5ab
# Parent  0bbf0d2348f9e026363ec5cd9be0f5a1ca06fc65
added Term.fold_atyps_sorts convenience;

diff -r 0bbf0d2348f9 -r b7fcca3d9a44 src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Mar 27 15:20:31 2010 +0100
+++ b/src/Pure/term.ML	Sat Mar 27 15:47:57 2010 +0100
@@ -72,6 +72,7 @@
   val map_type_tfree: (string * sort -> typ) -> typ -> typ
   val map_types: (typ -> typ) -> term -> term
   val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
+  val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
@@ -431,6 +432,9 @@
 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   | fold_atyps f T = f T;
 
+fun fold_atyps_sorts f =
+  fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S));
+
 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   | fold_aterms f a = f a;
diff -r 0bbf0d2348f9 -r b7fcca3d9a44 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Mar 27 15:20:31 2010 +0100
+++ b/src/Pure/thm.ML	Sat Mar 27 15:47:57 2010 +0100
@@ -484,10 +484,7 @@
   | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
       let
         val thy = Theory.deref thy_ref;
-        val present =
-          (fold_terms o fold_types o fold_atyps)
-            (fn T as TFree (_, S) => insert (eq_snd op =) (T, S)
-              | T as TVar (_, S) => insert (eq_snd op =) (T, S)) thm [];
+        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
         val extra = fold (Sorts.remove_sort o #2) present shyps;
         val witnessed = Sign.witness_sorts thy present extra;
         val extra' = fold (Sorts.remove_sort o #2) witnessed extra