diff -r d4d47d08e16a -r 6067703399ad src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 16:48:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:04:39 2013 +0200
@@ -67,11 +67,12 @@
     (term list * (string * typ) list) * Proof.context
   val mk_Freess': string -> typ list list -> Proof.context ->
     (term list list * (string * typ) list list) * Proof.context
+  val nonzero_string_of_int: int -> string
   val retype_free: typ -> term -> term
+  val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
   val variant_types: string list -> sort list -> Proof.context ->
     (string * sort) list * Proof.context
   val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
-  val nonzero_string_of_int: int -> string
 
   val num_binder_types: typ -> int
   val strip_typeN: int -> typ -> typ list * typ
@@ -374,6 +375,14 @@
 fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
 val mk_TFreess = fold_map mk_TFrees;
 
+(*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
+fun typ_subst_nonatomic [] = I
+  | typ_subst_nonatomic inst =
+    let
+      fun subst (Type (s, Ts)) = perhaps (AList.lookup (op =) inst) (Type (s, map subst Ts))
+        | subst T = perhaps (AList.lookup (op =) inst) T;
+    in subst end;
+
 fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n);
 
 fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names;