# HG changeset patch
# User wenzelm
# Date 1188479081 -7200
# Node ID 0b1a8fd26da98135f8f54efed8f7d33583e39f7d
# Parent  5edb9a54900f0b837cdea867a9c1a7636066dc41
added burrow_types;

diff -r 5edb9a54900f -r 0b1a8fd26da9 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Aug 30 11:46:37 2007 +0200
+++ b/src/Pure/term.ML	Thu Aug 30 15:04:41 2007 +0200
@@ -74,6 +74,7 @@
   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
+  val burrow_types: (typ list -> typ list) -> term list -> term list
   val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
   val add_term_names: term * string list -> string list
   val aconv: term * term -> bool
@@ -481,6 +482,26 @@
 
 fun fold_types f = fold_term_types (K f);
 
+fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts)
+  | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts)
+  | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts)
+  | replace_types (Bound i) Ts = (Bound i, Ts)
+  | replace_types (Abs (x, _, b)) (T :: Ts) =
+      let val (b', Ts') = replace_types b Ts
+      in (Abs (x, T, b'), Ts') end
+  | replace_types (t $ u) Ts =
+      let
+        val (t', Ts') = replace_types t Ts;
+        val (u', Ts'') = replace_types u Ts';
+      in (t' $ u', Ts'') end;
+
+fun burrow_types f ts =
+  let
+    val Ts = rev (fold (fold_types cons) ts []);
+    val Ts' = f Ts;
+    val (ts', []) = fold_map replace_types ts Ts';
+  in ts' end;
+
 (*collect variables*)
 val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
 val add_tvars = fold_types add_tvarsT;