honor user-specified name for relator + generalize syntax
authorblanchet
Wed Apr 24 18:49:52 2013 +0200 (2013-04-24)
changeset 51767bbcdd8519253
parent 51766 f19a4d0ab1bf
child 51768 d2a236b10796
honor user-specified name for relator + generalize syntax
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_fp.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_util.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 17:47:22 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 18:49:52 2013 +0200
     1.3 @@ -262,7 +262,7 @@
     1.4  
     1.5      val (bnf', lthy') =
     1.6        bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
     1.7 -        [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
     1.8 +        Binding.empty [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
     1.9    in
    1.10      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.11    end;
    1.12 @@ -360,7 +360,7 @@
    1.13  
    1.14      val (bnf', lthy') =
    1.15        bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
    1.16 -        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.17 +        Binding.empty [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.18    in
    1.19      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.20    end;
    1.21 @@ -443,8 +443,8 @@
    1.22      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.23  
    1.24      val (bnf', lthy') =
    1.25 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
    1.26 -        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.27 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
    1.28 +        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.29  
    1.30    in
    1.31      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.32 @@ -520,8 +520,8 @@
    1.33      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.34  
    1.35      val (bnf', lthy') =
    1.36 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
    1.37 -        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.38 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
    1.39 +        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.40    in
    1.41      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.42    end;
    1.43 @@ -663,7 +663,7 @@
    1.44      fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
    1.45  
    1.46      val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
    1.47 -      Binding.empty []
    1.48 +      Binding.empty Binding.empty []
    1.49        (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
    1.50    in
    1.51      ((bnf', deads), lthy')
     2.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 17:47:22 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 18:49:52 2013 +0200
     2.3 @@ -94,7 +94,8 @@
     2.4    val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
     2.5      ({prems: thm list, context: Proof.context} -> tactic) list ->
     2.6      ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
     2.7 -    binding list -> ((((binding * term) * term list) * term) * term list) * term option ->
     2.8 +    binding -> binding list ->
     2.9 +    ((((binding * term) * term list) * term) * term list) * term option ->
    2.10      local_theory -> BNF * local_theory
    2.11  end;
    2.12  
    2.13 @@ -544,7 +545,7 @@
    2.14  
    2.15  (* Define new BNFs *)
    2.16  
    2.17 -fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b set_bs
    2.18 +fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b rel_b set_bs
    2.19    (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy =
    2.20    let
    2.21      val fact_policy = mk_fact_policy no_defs_lthy;
    2.22 @@ -766,7 +767,9 @@
    2.23            (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, sQs)))
    2.24        | SOME raw_rel => prep_term no_defs_lthy raw_rel);
    2.25  
    2.26 -    val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
    2.27 +    val rel_bind_def =
    2.28 +      (fn () => if Binding.is_empty rel_b then Binding.suffix_name ("_" ^ relN) b else rel_b,
    2.29 +       rel_rhs);
    2.30  
    2.31      val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) =
    2.32        lthy
    2.33 @@ -1261,7 +1264,7 @@
    2.34  fun mk_conjunction_balanced' [] = @{prop True}
    2.35    | mk_conjunction_balanced' ts = Logic.mk_conjunction_balanced ts;
    2.36  
    2.37 -fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds =
    2.38 +fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
    2.39    (fn (_, goals, wit_goalss, after_qed, lthy, one_step_defs) =>
    2.40    let
    2.41      val wits_tac =
    2.42 @@ -1277,13 +1280,14 @@
    2.43      map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
    2.44        goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs)
    2.45      |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
    2.46 -  end) oooo prepare_def const_policy fact_policy qualify (K I) Ds;
    2.47 +  end) oo prepare_def const_policy fact_policy qualify (K I) Ds map_b rel_b set_bs;
    2.48  
    2.49  val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
    2.50    Proof.unfolding ([[(defs, [])]])
    2.51      (Proof.theorem NONE (snd o register_bnf key oo after_qed)
    2.52        (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
    2.53 -  prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE Binding.empty [];
    2.54 +  prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE Binding.empty Binding.empty
    2.55 +    [];
    2.56  
    2.57  fun print_bnfs ctxt =
    2.58    let
     3.1 --- a/src/HOL/BNF/Tools/bnf_fp.ML	Wed Apr 24 17:47:22 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp.ML	Wed Apr 24 18:49:52 2013 +0200
     3.3 @@ -141,9 +141,10 @@
     3.4    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
     3.5  
     3.6    val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list ->
     3.7 -      binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
     3.8 -    binding list -> mixfix list -> binding list -> binding list list -> (string * sort) list ->
     3.9 -    ((string * sort) * typ) list -> local_theory -> BNF_Def.BNF list * 'a
    3.10 +      binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
    3.11 +      local_theory -> 'a) ->
    3.12 +    binding list -> mixfix list -> binding list -> binding list -> binding list list ->
    3.13 +    (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.BNF list * 'a
    3.14  end;
    3.15  
    3.16  structure BNF_FP : BNF_FP =
    3.17 @@ -386,8 +387,8 @@
    3.18    | fp_sort lhss (SOME resBs) Ass =
    3.19      (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
    3.20  
    3.21 -fun mk_fp_bnf timer construct_fp resBs bs map_bs set_bss sort lhss bnfs deadss livess unfold_set
    3.22 -    lthy =
    3.23 +fun mk_fp_bnf timer construct_fp resBs bs map_bs rel_bs set_bss sort lhss bnfs deadss livess
    3.24 +    unfold_set lthy =
    3.25    let
    3.26      val name = mk_common_name (map Binding.name_of bs);
    3.27      fun qualify i =
    3.28 @@ -415,14 +416,14 @@
    3.29  
    3.30      val timer = time (timer "Normalization & sealing of BNFs");
    3.31  
    3.32 -    val res = construct_fp resBs bs map_bs set_bss (map TFree resDs, deadss) bnfs'' lthy'';
    3.33 +    val res = construct_fp resBs bs map_bs rel_bs set_bss (map TFree resDs, deadss) bnfs'' lthy'';
    3.34  
    3.35      val timer = time (timer "FP construction in total");
    3.36    in
    3.37      timer; (bnfs'', res)
    3.38    end;
    3.39  
    3.40 -fun fp_bnf construct_fp bs mixfixes map_bs set_bss resBs eqs lthy =
    3.41 +fun fp_bnf construct_fp bs mixfixes map_bs rel_bs set_bss resBs eqs lthy =
    3.42    let
    3.43      val timer = time (Timer.startRealTimer ());
    3.44      val (lhss, rhss) = split_list eqs;
    3.45 @@ -432,8 +433,8 @@
    3.46        (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
    3.47          (empty_unfolds, lthy));
    3.48    in
    3.49 -    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs map_bs set_bss sort lhss bnfs Dss Ass
    3.50 -      unfold_set lthy'
    3.51 +    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs map_bs rel_bs set_bss sort lhss bnfs Dss
    3.52 +      Ass unfold_set lthy'
    3.53    end;
    3.54  
    3.55  end;
     4.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 17:47:22 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 18:49:52 2013 +0200
     4.3 @@ -8,15 +8,15 @@
     4.4  signature BNF_FP_DEF_SUGAR =
     4.5  sig
     4.6    val datatypes: bool ->
     4.7 -    (mixfix list -> (string * sort) list option -> binding list -> binding list ->
     4.8 +    (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
     4.9        binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    4.10        BNF_FP.fp_result * local_theory) ->
    4.11 -    (bool * bool) * ((((binding * (binding * (typ * sort)) list) * binding) * mixfix) *
    4.12 +    (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
    4.13        ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    4.14          mixfix) list) list ->
    4.15      local_theory -> local_theory
    4.16    val parse_datatype_cmd: bool ->
    4.17 -    (mixfix list -> (string * sort) list option -> binding list -> binding list ->
    4.18 +    (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
    4.19        binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    4.20        BNF_FP.fp_result * local_theory) ->
    4.21      (local_theory -> local_theory) parser
    4.22 @@ -130,9 +130,10 @@
    4.23    reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
    4.24    handle THM _ => thm;
    4.25  
    4.26 -fun map_binding_of ((((b, _), _), _), _) = b;
    4.27 -fun type_args_named_constrained_of ((((_, ncAs), _), _), _) = ncAs;
    4.28 -fun type_binding_of (((_, b), _), _) = b;
    4.29 +fun type_args_named_constrained_of ((((ncAs, _), _), _), _) = ncAs;
    4.30 +fun type_binding_of ((((_, b), _), _), _) = b;
    4.31 +fun map_binding_of (((_, (b, _)), _), _) = b;
    4.32 +fun rel_binding_of (((_, (_, b)), _), _) = b;
    4.33  fun mixfix_of ((_, mx), _) = mx;
    4.34  fun ctr_specs_of (_, ctr_specs) = ctr_specs;
    4.35  
    4.36 @@ -159,6 +160,7 @@
    4.37      val fp_b_names = map Binding.name_of fp_bs;
    4.38      val fp_common_name = mk_common_name fp_b_names;
    4.39      val map_bs = map map_binding_of specs;
    4.40 +    val rel_bs = map rel_binding_of specs;
    4.41  
    4.42      fun prepare_type_arg (_, (ty, c)) =
    4.43        let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
    4.44 @@ -244,7 +246,7 @@
    4.45      val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
    4.46             fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
    4.47             fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
    4.48 -      fp_bnf construct_fp fp_bs mixfixes map_bs set_bss (map dest_TFree unsorted_As) fp_eqs
    4.49 +      fp_bnf construct_fp fp_bs mixfixes map_bs rel_bs set_bss (map dest_TFree unsorted_As) fp_eqs
    4.50          no_defs_lthy0;
    4.51  
    4.52      val timer = time (Timer.startRealTimer ());
    4.53 @@ -1196,13 +1198,31 @@
    4.54    @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
    4.55    Scan.succeed [];
    4.56  
    4.57 -val parse_single_spec =
    4.58 -  parse_opt_binding_colon -- parse_type_args_named_constrained -- Parse.binding --
    4.59 -  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon --
    4.60 -      Parse.binding -- Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] --
    4.61 -    Parse.opt_mixfix));
    4.62 +val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- Parse.binding;
    4.63 +
    4.64 +val no_map_rel = (Binding.empty, Binding.empty);
    4.65 +
    4.66 +(* "map" and "rel" are purposedly not registered as keywords, because they are short and nice names
    4.67 +   that we don't want them to be highlighted everywhere because of some obscure feature of the BNF
    4.68 +   package. *)
    4.69 +fun extract_map_rel ("map", b) = apfst (K b)
    4.70 +  | extract_map_rel ("rel", b) = apsnd (K b)
    4.71 +  | extract_map_rel (s, _) = error ("Expected \"map\" or \"rel\" instead of " ^ quote s);
    4.72  
    4.73 -val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
    4.74 +val parse_map_rel_bindings =
    4.75 +  @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"}
    4.76 +    >> (fn ps => fold extract_map_rel ps no_map_rel) ||
    4.77 +  Scan.succeed no_map_rel;
    4.78 +
    4.79 +val parse_ctr_spec =
    4.80 +  parse_opt_binding_colon -- Parse.binding -- Scan.repeat parse_ctr_arg --
    4.81 +  Scan.optional parse_defaults [] -- Parse.opt_mixfix;
    4.82 +
    4.83 +val parse_spec =
    4.84 +  parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
    4.85 +  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
    4.86 +
    4.87 +val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;
    4.88  
    4.89  fun parse_datatype_cmd lfp construct_fp = parse_datatype >> datatype_cmd lfp construct_fp;
    4.90  
     5.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 17:47:22 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 18:49:52 2013 +0200
     5.3 @@ -10,8 +10,8 @@
     5.4  signature BNF_GFP =
     5.5  sig
     5.6    val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
     5.7 -    binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     5.8 -    BNF_FP.fp_result * local_theory
     5.9 +    binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
    5.10 +    local_theory -> BNF_FP.fp_result * local_theory
    5.11  end;
    5.12  
    5.13  structure BNF_GFP : BNF_GFP =
    5.14 @@ -55,7 +55,7 @@
    5.15       ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
    5.16  
    5.17  (*all BNFs have the same lives*)
    5.18 -fun construct_gfp mixfixes resBs bs map_bs set_bss (resDs, Dss) bnfs lthy =
    5.19 +fun construct_gfp mixfixes resBs bs map_bs rel_bs set_bss (resDs, Dss) bnfs lthy =
    5.20    let
    5.21      val timer = time (Timer.startRealTimer ());
    5.22  
    5.23 @@ -2894,13 +2894,13 @@
    5.24          val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs);
    5.25  
    5.26          val (Jbnfs, lthy) =
    5.27 -          fold_map8 (fn tacs => fn b => fn map_b => fn set_bs => fn mapx => fn sets => fn T =>
    5.28 -              fn (thms, wits) => fn lthy =>
    5.29 +          fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
    5.30 +              fn T => fn (thms, wits) => fn lthy =>
    5.31              bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) map_b
    5.32 -              set_bs (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
    5.33 -              lthy
    5.34 +              rel_b set_bs
    5.35 +              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
    5.36              |> register_bnf (Local_Theory.full_name lthy b))
    5.37 -          tacss bs map_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy;
    5.38 +          tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy;
    5.39  
    5.40          val fold_maps = fold_thms lthy (map (fn bnf =>
    5.41            mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs);
     6.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 17:47:22 2013 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 18:49:52 2013 +0200
     6.3 @@ -9,8 +9,8 @@
     6.4  signature BNF_LFP =
     6.5  sig
     6.6    val construct_lfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
     6.7 -    binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     6.8 -    BNF_FP.fp_result * local_theory
     6.9 +    binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
    6.10 +    local_theory -> BNF_FP.fp_result * local_theory
    6.11  end;
    6.12  
    6.13  structure BNF_LFP : BNF_LFP =
    6.14 @@ -26,7 +26,7 @@
    6.15  open BNF_LFP_Tactics
    6.16  
    6.17  (*all BNFs have the same lives*)
    6.18 -fun construct_lfp mixfixes resBs bs map_bs set_bss (resDs, Dss) bnfs lthy =
    6.19 +fun construct_lfp mixfixes resBs bs map_bs rel_bs set_bss (resDs, Dss) bnfs lthy =
    6.20    let
    6.21      val timer = time (Timer.startRealTimer ());
    6.22  
    6.23 @@ -1734,12 +1734,13 @@
    6.24          fun wit_tac _ = mk_wit_tac n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
    6.25  
    6.26          val (Ibnfs, lthy) =
    6.27 -          fold_map8 (fn tacs => fn b => fn map_b => fn set_bs => fn mapx => fn sets => fn T =>
    6.28 -              fn wits => fn lthy =>
    6.29 -            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) map_b set_bs
    6.30 -              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
    6.31 +          fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
    6.32 +              fn T => fn wits => fn lthy =>
    6.33 +            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) map_b rel_b
    6.34 +              set_bs (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
    6.35 +              lthy
    6.36              |> register_bnf (Local_Theory.full_name lthy b))
    6.37 -          tacss bs map_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
    6.38 +          tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
    6.39  
    6.40          val fold_maps = fold_thms lthy (map (fn bnf =>
    6.41            mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Ibnfs);
     7.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 17:47:22 2013 +0200
     7.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 18:49:52 2013 +0200
     7.3 @@ -43,6 +43,9 @@
     7.4    val fold_map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j * 'i) ->
     7.5      'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i ->
     7.6      'j list * 'i
     7.7 +  val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) ->
     7.8 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
     7.9 +    'i list -> 'j -> 'k list * 'j
    7.10    val splice: 'a list -> 'a list -> 'a list
    7.11    val transpose: 'a list list -> 'a list list
    7.12    val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
    7.13 @@ -286,6 +289,15 @@
    7.14      in (x :: xs, acc'') end
    7.15    | fold_map8 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    7.16  
    7.17 +fun fold_map9 _ [] [] [] [] [] [] [] [] [] acc = ([], acc)
    7.18 +  | fold_map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
    7.19 +      (x9::x9s) acc =
    7.20 +    let
    7.21 +      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 x9 acc;
    7.22 +      val (xs, acc'') = fold_map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s acc';
    7.23 +    in (x :: xs, acc'') end
    7.24 +  | fold_map9 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    7.25 +
    7.26  (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
    7.27  fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
    7.28  fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);