# HG changeset patch
# User traytel
# Date 1377763735 -7200
# Node ID 876ce6767d6801fd02577056866d461591973d2d
# Parent  d6d813d7e702874207f27f0f2f8e05e9ac9da0e7
build relator term for compound type (generalized build_map)

diff -r d6d813d7e702 -r 876ce6767d68 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 08:05:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 10:08:55 2013 +0200
@@ -35,7 +35,9 @@
   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
   val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
@@ -270,11 +272,13 @@
     Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   end;
 
-fun build_map lthy build_simple =
+local
+
+fun build_map_or_rel mk const of_bnf dest lthy build_simple =
   let
     fun build (TU as (T, U)) =
       if T = U then
-        HOLogic.id_const T
+        const T
       else
         (case TU of
           (Type (s, Ts), Type (s', Us)) =>
@@ -282,14 +286,21 @@
             let
               val bnf = the (bnf_of lthy s);
               val live = live_of_bnf bnf;
-              val mapx = mk_map live Ts Us (map_of_bnf bnf);
-              val TUs' = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
+              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;
 
+in
+
+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;
+
+end;
+
 fun fo_match ctxt t pat =
   let val thy = Proof_Context.theory_of ctxt in
     Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)