1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 18:04:39 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 18:06:37 2013 +0200
     1.3 @@ -177,8 +177,6 @@
     1.4  
     1.5  val exists_subtype_in = Term.exists_subtype o member (op =);
     1.6  
     1.7 -fun resort_tfree S (TFree (s, _)) = TFree (s, S);
     1.8 -
     1.9  val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
    1.10  
    1.11  fun flat_rec_arg_args xss =

     2.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:04:39 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:06:37 2013 +0200
     2.3 @@ -68,6 +68,7 @@
     2.4    val mk_Freess': string -> typ list list -> Proof.context ->
     2.5      (term list list * (string * typ) list list) * Proof.context
     2.6    val nonzero_string_of_int: int -> string
     2.7 +  val resort_tfree: sort -> typ -> typ
     2.8    val retype_free: typ -> term -> term
     2.9    val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
    2.10    val variant_types: string list -> sort list -> Proof.context ->
    2.11 @@ -375,6 +376,8 @@
    2.12  fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
    2.13  val mk_TFreess = fold_map mk_TFrees;
    2.14  
    2.15 +fun resort_tfree S (TFree (s, _)) = TFree (s, S);
    2.16 +
    2.17  (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
    2.18  fun typ_subst_nonatomic [] = I
    2.19    | typ_subst_nonatomic inst =