# HG changeset patch
# User blanchet
# Date 1399271438 -7200
# Node ID aa2de99be748663116af79c4e3fe554ee99422fc
# Parent  d940ad3959c513a6d6f04ab2597acb148f1bd7e1
note correct induction schemes in 'primrec' (for N2M)

diff -r d940ad3959c5 -r aa2de99be748 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun May 04 21:35:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon May 05 08:30:38 2014 +0200
@@ -136,7 +136,7 @@
     val thy = Proof_Context.theory_of lthy0;
 
     val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps,
-         induct_thm, n2m, lthy) =
+         common_induct, n2m, lthy) =
       get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0;
 
     val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
@@ -159,7 +159,7 @@
     fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
     fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
 
-    val induct_thms = unpermute0 (conj_dests nn induct_thm);
+    val inducts = unpermute0 (conj_dests nn common_induct);
 
     val lfpTs = unpermute perm_lfpTs;
     val Cs = unpermute perm_Cs;
@@ -198,8 +198,7 @@
        nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
        ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
   in
-    ((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, induct_thm, induct_thms),
-     lthy)
+    ((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, common_induct, inducts), lthy)
   end;
 
 val undef_const = Const (@{const_name undefined}, dummyT);
@@ -452,7 +451,7 @@
         [] => ()
       | (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", []));
 
-    val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy) =
+    val ((n2m, rec_specs, _, common_induct, inducts), lthy) =
       rec_specs_of bs arg_Ts res_Ts frees callssss lthy0;
 
     val actual_nn = length funs_data;
@@ -493,8 +492,7 @@
 
     val notes =
       (if n2m then
-         map2 (fn name => fn thm => (name, inductN, [thm], [])) fun_names
-           (take actual_nn induct_thms)
+         map2 (fn name => fn thm => (name, inductN, [thm], [])) fun_names (take actual_nn inducts)
        else
          [])
       |> map (fn (prefix, thmN, thms, attrs) =>
@@ -503,7 +501,7 @@
     val common_name = mk_common_name fun_names;
 
     val common_notes =
-      (if n2m then [(inductN, [induct_thm], [])] else [])
+      (if n2m then [(inductN, [common_induct], [])] else [])
       |> map (fn (thmN, thms, attrs) =>
         ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
   in
diff -r d940ad3959c5 -r aa2de99be748 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Sun May 04 21:35:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Mon May 05 08:30:38 2014 +0200
@@ -29,8 +29,8 @@
 fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
   let
     val ((missing_arg_Ts, perm0_kks,
-          fp_sugars as {nested_bnfs, co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)),
-         lthy) =
+          fp_sugars as {nested_bnfs, common_co_inducts = [common_induct], ...} :: _,
+          (lfp_sugar_thms, _)), lthy) =
       nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
 
     val Ts = map #T fp_sugars;
@@ -51,7 +51,7 @@
     val nested_map_comps = map map_comp_of_bnf nested_bnfs;
   in
     (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
-     nested_map_idents, nested_map_comps, induct_thm, is_some lfp_sugar_thms, lthy)
+     nested_map_idents, nested_map_comps, common_induct, is_some lfp_sugar_thms, lthy)
   end;
 
 exception NOT_A_MAP of term;