# HG changeset patch
# User blanchet
# Date 1376669079 -7200
# Node ID 6067703399adab44fd9fc40dc2f5c6c8ee9ccdf3
# Parent  d4d47d08e16a193c6574c10a79ad91619c0959e5
moved library function where it belongs, and used Dmitriy's inside-out implementation

diff -r d4d47d08e16a -r 6067703399ad src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 16:48:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 18:04:39 2013 +0200
@@ -179,14 +179,6 @@
 
 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
 
-(* FIXME: merge with function of the same name in "bnf_fp_n2m.ML" (in the
-   prim(co)rec repository) *)
-fun typ_subst_nonatomic inst (T as Type (s, Ts)) =
-    (case AList.lookup (op =) inst T of
-      NONE => Type (s, map (typ_subst_nonatomic inst) Ts)
-    | SOME T' => T')
-  | typ_subst_nonatomic inst T = the_default T (AList.lookup (op =) inst T);
-
 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
 
 fun flat_rec_arg_args xss =
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;