# HG changeset patch
# User blanchet
# Date 1482317116 -3600
# Node ID f6d0578b46c9b4f36f4c495dc54d6717a45958a0
# Parent  c6330e16743fbe49119b2bd1fbe10614f2b63a72
generalized ML function (towards nonuniform datatypes)

diff -r c6330e16743f -r f6d0578b46c9 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Dec 21 11:14:55 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Dec 21 11:45:16 2016 +0100
@@ -163,8 +163,8 @@
       * (((term list list * term list list * term list list list list * term list list list list)
           * term list list list) * typ list) -> (string -> binding) -> 'b list -> typ list ->
     term list -> term -> local_theory -> (term * thm) * local_theory
-  val mk_induct_raw_prem: Proof.context -> typ list list -> (string * term list) list -> term ->
-    term -> typ list -> typ list ->
+  val mk_induct_raw_prem: (term -> term) -> Proof.context -> typ list list ->
+    (string * term list) list -> term -> term -> typ list -> typ list ->
     term list * ((term * (term * term)) list * (int * term)) list * term
   val finish_induct_prem: Proof.context -> int -> term list ->
     term list * ((term * (term * term)) list * (int * term)) list * term -> term
@@ -1643,12 +1643,12 @@
     [([], (find_index (fn Xs => member (op =) Xs X) Xss + 1, x))]
   | mk_induct_raw_prem_prems _ _ _ _ _ = [];
 
-fun mk_induct_raw_prem names_lthy Xss setss_fp_nesting p ctr ctr_Ts ctrXs_Ts =
+fun mk_induct_raw_prem modify_x names_lthy Xss setss_fp_nesting p ctr ctr_Ts ctrXs_Ts =
   let
     val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
     val pprems =
       flat (map2 (mk_induct_raw_prem_prems names_lthy' Xss setss_fp_nesting) xs ctrXs_Ts);
-    val y = Term.list_comb (ctr, xs);
+    val y = Term.list_comb (ctr, map modify_x xs);
     val p' = enforce_type names_lthy domain_type (fastype_of y) p;
   in (xs, pprems, HOLogic.mk_Trueprop (p' $ y)) end;
 
@@ -1750,7 +1750,7 @@
     val (induct_thms, induct_thm) =
       let
         val raw_premss = @{map 4} (@{map 3}
-            o mk_induct_raw_prem names_lthy (map single Xs) setss_fp_nesting)
+            o mk_induct_raw_prem I names_lthy (map single Xs) setss_fp_nesting)
           ps ctrss ctr_Tsss ctrXs_Tsss;
         val concl =
           HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us));