# HG changeset patch
# User blanchet
# Date 1376669197 -7200
# Node ID b139670d88d929e14cc22b3862b2224fa1eb8536
# Parent  6067703399adab44fd9fc40dc2f5c6c8ee9ccdf3
moved function to where it seems to belong

diff -r 6067703399ad -r b139670d88d9 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 18:04:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 18:06:37 2013 +0200
@@ -177,8 +177,6 @@
 
 val exists_subtype_in = Term.exists_subtype o member (op =);
 
-fun resort_tfree S (TFree (s, _)) = TFree (s, S);
-
 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
 
 fun flat_rec_arg_args xss =
diff -r 6067703399ad -r b139670d88d9 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:04:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:06:37 2013 +0200
@@ -68,6 +68,7 @@
   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 resort_tfree: sort -> typ -> typ
   val retype_free: typ -> term -> term
   val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
   val variant_types: string list -> sort list -> Proof.context ->
@@ -375,6 +376,8 @@
 fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
 val mk_TFreess = fold_map mk_TFrees;
 
+fun resort_tfree S (TFree (s, _)) = TFree (s, S);
+
 (*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
 fun typ_subst_nonatomic [] = I
   | typ_subst_nonatomic inst =