updated to infer_instantiate;

--- 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)

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sun Jul 26 20:56:44 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Sun Jul 26 20:57:35 2015 +0200
@@ -63,7 +63,6 @@
 
   val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv
 
-  val cterm_instantiate_pos: cterm option list -> thm -> thm
   val unfold_thms: Proof.context -> thm list -> thm -> thm
 
   val name_noted_thms: string -> string -> (string * thm list) list -> (string * thm list) list
@@ -212,22 +211,8 @@
 val list_exists_free = list_quant_free HOLogic.exists_const;
 
 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)
-  end;
-
-fun cterm_instantiate_pos cts thm =
-  let
-    val thy = Thm.theory_of_thm thm;
-    val vars = Term.add_vars (Thm.prop_of thm) [];
-    val vars' = rev (drop (length vars - length cts) vars);
-    val ps =
-      map_filter
-        (fn (_, NONE) => NONE
-          | (var, SOME ct) => SOME (Thm.global_cterm_of thy (Var var), ct)) (vars' ~~ cts);
-  in
-    Drule.cterm_instantiate ps thm
-  end;
+  let val thy = Proof_Context.theory_of ctxt
+  in Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty) end;
 
 fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);