--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Sun Jul 26 20:56:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Sun Jul 26 20:57:35 2015 +0200
@@ -190,10 +190,12 @@
val extract =
case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb);
val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts;
- val thetas = AList.group (op =)
- (mutual_cliques ~~ map (apply2 (Thm.cterm_of lthy)) (raw_phis ~~ pre_phis));
+ val thetas =
+ AList.group (op =)
+ (mutual_cliques ~~
+ map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of lthy u)) (raw_phis ~~ pre_phis));
in
- map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas)
+ map2 (infer_instantiate lthy o the o AList.lookup (op =) thetas)
mutual_cliques rel_xtor_co_inducts
end
@@ -214,13 +216,14 @@
fun mk_Grp_id P =
let val T = domain_type (fastype_of P);
in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
- val cts = map (SOME o Thm.cterm_of lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
+ val cts =
+ map (SOME o Thm.cterm_of names_lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
fun mk_fp_type_copy_thms thm = map (curry op RS thm)
@{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep};
fun mk_type_copy_thms thm = map (curry op RS thm)
@{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
in
- cterm_instantiate_pos cts xtor_rel_co_induct
+ infer_instantiate' names_lthy cts xtor_rel_co_induct
|> singleton (Proof_Context.export names_lthy lthy)
|> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @
fp_or_nesting_rel_eqs)
@@ -237,7 +240,7 @@
let
val cts = NONE :: map (SOME o Thm.cterm_of lthy) (map HOLogic.eq_const As);
in
- cterm_instantiate_pos cts xtor_rel_co_induct
+ infer_instantiate' lthy cts xtor_rel_co_induct
|> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
fp_or_nesting_rel_eqs)
|> funpow (2 * n) (fn thm => thm RS spec)