# HG changeset patch
# User blanchet
# Date 1383558761 -3600
# Node ID e000095237279f75af3da934148b1add59d98ac7
# Parent  3aed2ae6eb915952d5f9b3fafd15526d4049ca15
moved code around

diff -r 3aed2ae6eb91 -r e00009523727 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Nov 04 10:52:41 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Nov 04 10:52:41 2013 +0100
@@ -77,6 +77,11 @@
   val wit_thms_of_bnf: bnf -> thm list
   val wit_thmss_of_bnf: bnf -> thm list list
 
+  val mk_map: int -> typ list -> typ list -> term -> term
+  val mk_rel: int -> typ list -> typ list -> term -> term
+  val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
+  val build_rel: local_theory -> (typ * typ -> term) -> typ * typ -> term
+
   val mk_witness: int list * term -> thm list -> nonemptiness_witness
   val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
   val wits_of_bnf: bnf -> nonemptiness_witness list
@@ -447,7 +452,6 @@
   #> Option.map (morph_bnf (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
 
 
-
 (* Utilities *)
 
 fun normalize_set insts instA set =
@@ -487,6 +491,38 @@
        else minimize ((I, wit) :: done) todo;
  in minimize [] wits end;
 
+fun mk_map live Ts Us t =
+  let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
+    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
+  end;
+
+fun mk_rel live Ts Us t =
+  let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in
+    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
+  end;
+
+fun build_map_or_rel mk const of_bnf dest lthy build_simple =
+  let
+    fun build (TU as (T, U)) =
+      if T = U then
+        const T
+      else
+        (case TU of
+          (Type (s, Ts), Type (s', Us)) =>
+          if s = s' then
+            let
+              val bnf = the (bnf_of lthy s);
+              val live = live_of_bnf bnf;
+              val mapx = mk live Ts Us (of_bnf bnf);
+              val TUs' = map dest (fst (strip_typeN live (fastype_of mapx)));
+            in Term.list_comb (mapx, map build TUs') end
+          else
+            build_simple TU
+        | _ => build_simple TU);
+  in build end;
+
+val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT;
+val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T;
 
 
 (* Names *)
diff -r 3aed2ae6eb91 -r e00009523727 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
@@ -39,10 +39,6 @@
     'a list
   val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
   val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
-  val mk_map: int -> typ list -> typ list -> term -> term
-  val mk_rel: int -> typ list -> typ list -> term -> term
-  val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
-  val build_rel: local_theory -> (typ * typ -> term) -> typ * typ -> term
   val dest_map: Proof.context -> string -> term -> term * term list
   val dest_ctr: Proof.context -> string -> term -> term * term list
 
@@ -290,39 +286,6 @@
   | unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts
   | unzip_corecT _ T = [T];
 
-fun mk_map live Ts Us t =
-  let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
-    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
-  end;
-
-fun mk_rel live Ts Us t =
-  let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in
-    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
-  end;
-
-fun build_map_or_rel mk const of_bnf dest lthy build_simple =
-  let
-    fun build (TU as (T, U)) =
-      if T = U then
-        const T
-      else
-        (case TU of
-          (Type (s, Ts), Type (s', Us)) =>
-          if s = s' then
-            let
-              val bnf = the (bnf_of lthy s);
-              val live = live_of_bnf bnf;
-              val mapx = mk live Ts Us (of_bnf bnf);
-              val TUs' = map dest (fst (strip_typeN live (fastype_of mapx)));
-            in Term.list_comb (mapx, map build TUs') end
-          else
-            build_simple TU
-        | _ => build_simple TU);
-  in build end;
-
-val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT;
-val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T;
-
 val dummy_var_name = "?f"
 
 fun mk_map_pattern ctxt s =