# HG changeset patch
# User wenzelm
# Date 1437924294 -7200
# Node ID 4f590c08fd5d2ceae916c169a5a4c62bd823b138
# Parent  495bede1c4d9b16e3f51e1a1b90d555b9947d726
updated to infer_instantiate;

diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -1368,7 +1368,7 @@
           let
             val rel_conversep_thm = Lazy.force rel_conversep;
             val cts = map (SOME o Thm.cterm_of lthy) Rs;
-            val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
+            val rel_conversep_thm' = infer_instantiate' lthy cts rel_conversep_thm;
           in
             unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_eqD})
             |> singleton (Proof_Context.export names_lthy pre_names_lthy)
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -473,13 +473,12 @@
 fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) =
   Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1));
 
-fun flip_rels lthy n thm =
+fun flip_rels ctxt n thm =
   let
     val Rs = Term.add_vars (Thm.prop_of thm) [];
     val Rs' = rev (drop (length Rs - n) Rs);
-    val cRs = map (fn f => (Thm.cterm_of lthy (Var f), Thm.cterm_of lthy (mk_flip f))) Rs';
   in
-    Drule.cterm_instantiate cRs thm
+    infer_instantiate ctxt (map (fn f => (fst f, Thm.cterm_of ctxt (mk_flip f))) Rs') thm
   end;
 
 fun mk_ctor_or_dtor get_T Ts t =
@@ -599,7 +598,7 @@
           Drule.dummy_thm
         else
           let val ctor' = mk_ctor Bs ctor in
-            cterm_instantiate_pos [NONE, NONE, SOME (Thm.cterm_of lthy ctor')] arg_cong
+            infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of lthy ctor')] arg_cong
           end;
 
       fun mk_cIn ctor k xs =
@@ -616,7 +615,7 @@
         fold_thms lthy [ctr_def']
           (unfold_thms lthy (o_apply :: pre_map_def ::
                (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @ abs_inverses)
-             (cterm_instantiate_pos (map (SOME o Thm.cterm_of lthy) fs @ [SOME cxIn])
+             (infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) fs @ [SOME cxIn])
                 (if fp = Least_FP then fp_map_thm
                  else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans))))
         |> singleton (Proof_Context.export names_lthy lthy);
@@ -626,7 +625,7 @@
           (unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @
                (if fp = Least_FP then [] else [dtor_ctor]) @ basic_sumprod_thms_set @
                @{thms UN_Un sup_assoc[THEN sym]} @ abs_inverses)
-             (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
+             (infer_instantiate' lthy [SOME cxIn] fp_set_thm))
         |> singleton (Proof_Context.export names_lthy lthy);
 
       fun mk_set0_thms fp_set_thm = map2 (mk_set0_thm fp_set_thm) ctr_defs' cxIns;
@@ -644,7 +643,7 @@
           (unfold_thms lthy (pre_rel_def :: abs_inverses @
                (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
                @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
-             (cterm_instantiate_pos (map (SOME o Thm.cterm_of lthy) Rs @ [SOME cxIn, SOME cyIn])
+             (infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) Rs @ [SOME cxIn, SOME cyIn])
                 fp_rel_thm))
         |> postproc
         |> singleton (Proof_Context.export names_lthy lthy);
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -96,11 +96,9 @@
   let
     val fs = Term.add_vars (Thm.prop_of thm) []
       |> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false);
-    fun mk_cfp (f as (_, T)) =
-      (Thm.cterm_of ctxt (Var f), Thm.cterm_of ctxt (mk_proj T (num_binder_types T) k));
-    val cfps = map mk_cfp fs;
+    fun mk_inst (xi, T) = (xi, Thm.cterm_of ctxt (mk_proj T (num_binder_types T) k));
   in
-    Drule.cterm_instantiate cfps thm
+    infer_instantiate ctxt (map mk_inst fs) thm
   end;
 
 val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs;
@@ -185,7 +183,7 @@
     rel_eqs =
   let
     val ctor_rec_transfers' =
-      map (cterm_instantiate_pos (map SOME (passives @ actives))) ctor_rec_transfers;
+      map (infer_instantiate' ctxt (map SOME (passives @ actives))) ctor_rec_transfers;
     val total_n = Integer.sum ns;
     val True = @{term True};
   in
@@ -288,8 +286,9 @@
     fun mk_unfold_corec_type_tac dtor_corec_transfer corec_def =
       let
         val active :: actives' = actives;
-        val dtor_corec_transfer' = cterm_instantiate_pos
-          (SOME active :: map SOME passives @ map SOME actives') dtor_corec_transfer;
+        val dtor_corec_transfer' =
+          infer_instantiate' ctxt
+            (SOME active :: map SOME passives @ map SOME actives') dtor_corec_transfer;
       in
         HEADGOAL Goal.conjunction_tac THEN REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
         unfold_thms_tac ctxt [corec_def] THEN
@@ -389,7 +388,7 @@
 
 fun mk_map_disc_iff_tac ctxt ct exhaust discs maps =
   TRYALL Goal.conjunction_tac THEN
-  ALLGOALS (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+  ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
     REPEAT_DETERM o hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt maps THEN
   unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
@@ -398,7 +397,7 @@
 
 fun mk_map_sel_tac ctxt ct exhaust discs maps sels map_id0s =
   TRYALL Goal.conjunction_tac THEN
-    ALLGOALS (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+    ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
       REPEAT_DETERM o hyp_subst_tac ctxt) THEN
     unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
       @{thms not_True_eq_False not_False_eq_True}) THEN
@@ -407,8 +406,8 @@
     ALLGOALS (rtac ctxt refl);
 
 fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs=
-  HEADGOAL (rtac ctxt (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
-    rtac ctxt (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
+  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW
+    rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW
       hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt (rel_eqs @ injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
     True_implies_equals conj_imp_eq_imp_imp} @
@@ -426,7 +425,7 @@
    EVERY (@{map 11} (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
      fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
       (rtac ctxt exhaust THEN_ALL_NEW (rtac ctxt exhaust THEN_ALL_NEW
-         (dtac ctxt (rotate_prems ~1 (cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct]
+         (dtac ctxt (rotate_prems ~1 (infer_instantiate' ctxt [NONE, NONE, NONE, NONE, SOME ct]
             @{thm arg_cong2} RS iffD1)) THEN'
           assume_tac ctxt THEN' assume_tac ctxt THEN' hyp_subst_tac ctxt THEN' dtac ctxt assm THEN'
           REPEAT_DETERM o etac ctxt conjE))) 1 THEN
@@ -445,7 +444,7 @@
   rtac ctxt ctor_rel_induct 1 THEN EVERY (@{map 6} (fn cterm => fn exhaust => fn ctor_defs =>
       fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse =>
         HEADGOAL (rtac ctxt exhaust THEN_ALL_NEW (rtac ctxt exhaust THEN_ALL_NEW
-          (rtac ctxt (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
+          (rtac ctxt (infer_instantiate' ctxt (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
             THEN' assume_tac ctxt THEN' assume_tac ctxt THEN' TRY o resolve_tac ctxt assms))) THEN
         unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
           @{thms id_bnf_def vimage2p_def}) THEN
@@ -457,8 +456,8 @@
     cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
 
 fun mk_rel_sel_tac ctxt ct1 ct2 exhaust discs sels rel_injects distincts rel_distincts rel_eqs =
-  HEADGOAL (rtac ctxt (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
-    rtac ctxt (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
+  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW
+    rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW
       hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt (sels @ rel_injects @ rel_eqs @
     @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @ ((discs @ distincts) RL [eqTrueI, eqFalseI]) @
@@ -473,7 +472,7 @@
 
 fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
   TRYALL Goal.conjunction_tac THEN
-    ALLGOALS (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+    ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
       REPEAT_DETERM o hyp_subst_tac ctxt) THEN
     unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
       @{thms not_True_eq_False not_False_eq_True}) THEN
@@ -485,7 +484,7 @@
       (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt));
 
 fun mk_set_cases_tac ctxt ct assms exhaust sets =
-  HEADGOAL (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN
+  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt sets THEN
   REPEAT_DETERM (HEADGOAL
     (eresolve_tac ctxt @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE'
@@ -509,12 +508,12 @@
           (etac ctxt FalseE)
       end;
     val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
-      |> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts;
+      |> map2 (fn ct => infer_instantiate' ctxt [NONE, SOME ct]) cts;
   in
     ALLGOALS (resolve_tac ctxt dtor_set_inducts) THEN
     TRYALL (resolve_tac ctxt exhausts' THEN_ALL_NEW
       (resolve_tac ctxt (map (fn ct => refl RS
-         cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
+         infer_instantiate' ctxt (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
         THEN' assume_tac ctxt THEN' hyp_subst_tac ctxt)) THEN
     unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
       @{thms id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert Un_empty_left
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -44,7 +44,7 @@
         val else_branch = Var (("e", j), T);
         val lam = Term.lambda cond (mk_If cond then_branch else_branch);
       in
-        cterm_instantiate_pos [SOME (Thm.cterm_of ctxt lam)] thm
+        infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt lam)] thm
       end;
 
     val transfer_rules =
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -2223,9 +2223,10 @@
 
           fun mk_helper_coind_thms fst concl cts =
             Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
-              (fn {context = ctxt, prems = _} => mk_rel_coinduct_coind_tac ctxt fst m
-                (cterm_instantiate_pos cts dtor_coinduct_thm) ks map_comps map_cong0s
-                map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms in_rels)
+              (fn {context = ctxt, prems = _} =>
+                mk_rel_coinduct_coind_tac ctxt fst m
+                  (infer_instantiate' ctxt cts dtor_coinduct_thm) ks map_comps map_cong0s
+                  map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms in_rels)
             |> Thm.close_derivation
             |> split_conj_thm
             |> Proof_Context.export names_lthy lthy;
@@ -2261,8 +2262,9 @@
           val helper_ind_thmss = if m = 0 then replicate n [] else
             @{map 4} (fn concl => fn j => fn set_induct => fn cts =>
               Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
-                (fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks
-                  dtor_unfold_thms set_mapss j (cterm_instantiate_pos cts set_induct))
+                (fn {context = ctxt, prems = _} =>
+                  mk_rel_coinduct_ind_tac ctxt m ks
+                    dtor_unfold_thms set_mapss j (infer_instantiate' ctxt cts set_induct))
               |> Thm.close_derivation
               |> split_conj_thm
               |> Proof_Context.export names_lthy lthy)
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -43,13 +43,9 @@
   let
     val num_frees = length frees;
     val fs = Term.add_vars (Thm.prop_of thm) [] |> filter (can dest_funT o snd);
-    fun find s = find_index (curry (op =) s) frees;
-    fun mk_cfp (f as ((s, _), T)) =
-      (Thm.cterm_of ctxt (Var f), Thm.cterm_of ctxt (mk_proj T num_frees (find s)));
-    val cfps = map mk_cfp fs;
-  in
-    Drule.cterm_instantiate cfps thm
-  end;
+    fun find x = find_index (curry (op =) x) frees;
+    fun mk_inst ((x, i), T) = ((x, i), Thm.cterm_of ctxt (mk_proj T num_frees (find x)));
+  in infer_instantiate ctxt (map mk_inst fs) thm end;
 
 val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs;
 
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -783,7 +783,8 @@
 
     val car_inits = map (mk_min_alg str_inits) ks;
 
-    val alg_init_thm = cterm_instantiate_pos (map (SOME o Thm.cterm_of lthy) str_inits) alg_min_alg_thm;
+    val alg_init_thm =
+      infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) str_inits) alg_min_alg_thm;
 
     val alg_select_thm = Goal.prove_sorry lthy [] []
       (HOLogic.mk_Trueprop (mk_Ball II
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -68,7 +68,7 @@
   IF_UNSOLVED (unfold_thms_tac ctxt @{thms id_def o_def} THEN HEADGOAL (rtac ctxt refl));
 
 fun mk_size_neq ctxt cts exhaust sizes =
-  HEADGOAL (rtac ctxt (Ctr_Sugar_Util.cterm_instantiate_pos (map SOME cts) exhaust)) THEN
+  HEADGOAL (rtac ctxt (infer_instantiate' ctxt (map SOME cts) exhaust)) THEN
   ALLGOALS (hyp_subst_tac ctxt) THEN
   Ctr_Sugar_Tactics.unfold_thms_tac ctxt (@{thm neq0_conv} :: sizes) THEN
   ALLGOALS (REPEAT_DETERM o (rtac ctxt @{thm zero_less_Suc} ORELSE' rtac ctxt @{thm trans_less_add2}));
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -376,7 +376,7 @@
       REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt CollectI,
       REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' assume_tac ctxt)];
     fun cong_tac ct map_cong0 = EVERY'
-      [rtac ctxt (map_cong0 RS cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong),
+      [rtac ctxt (map_cong0 RS infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong),
       REPEAT_DETERM_N m o rtac ctxt refl,
       REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)];
 
@@ -434,7 +434,7 @@
     CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses,
     CONJ_WRAP' (fn (ct, thm) =>
       EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
-        rtac ctxt (thm RS (cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong) RS sym),
+        rtac ctxt (thm RS (infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong) RS sym),
         EVERY' (map (fn Abs_inverse =>
           EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse),
             assume_tac ctxt])
@@ -559,7 +559,7 @@
 
     fun mk_set_nat cset ctor_map ctor_set set_nats =
       EVERY' [rtac ctxt trans, rtac ctxt @{thm image_cong}, rtac ctxt ctor_set, rtac ctxt refl, rtac ctxt sym,
-        rtac ctxt (trans OF [ctor_map RS cterm_instantiate_pos [NONE, NONE, SOME cset] arg_cong,
+        rtac ctxt (trans OF [ctor_map RS infer_instantiate' ctxt [NONE, NONE, SOME cset] arg_cong,
           ctor_set RS trans]),
         rtac ctxt sym, EVERY' (map (rtac ctxt) [trans, @{thm image_Un}, Un_cong]),
         rtac ctxt sym, rtac ctxt (nth set_nats (i - 1)),
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -99,7 +99,7 @@
 
 fun mk_disc_eq_case_tac ctxt ct exhaust discs distincts cases =
   HEADGOAL Goal.conjunction_tac THEN
-  ALLGOALS (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+  ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
     (hyp_subst_tac ctxt THEN'
      SELECT_GOAL (unfold_thms_tac ctxt (@{thms not_True_eq_False not_False_eq_True} @ cases @
        ((refl :: discs @ distincts) RL [eqTrueI, eqFalseI]))) THEN'
@@ -161,7 +161,7 @@
   end;
 
 fun mk_case_distrib_tac ctxt ct exhaust cases =
-  HEADGOAL (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust)) THEN
+  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust)) THEN
   ALLGOALS (hyp_subst_tac ctxt THEN' SELECT_GOAL (unfold_thms_tac ctxt cases) THEN' rtac ctxt refl);
 
 fun mk_case_cong_tac ctxt uexhaust cases =
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -107,17 +107,6 @@
 
 (*** Auxiliary functions ***)
 
-(*positional instantiation with computed type substitution.
-  internal version of  attribute "[of s t u]".*)
-fun cterm_instantiate' cts thm =
-  let
-    val thy = Thm.theory_of_thm thm;
-    val vs = rev (Term.add_vars (Thm.prop_of thm) [])
-      |> map (Thm.global_cterm_of thy o Var);
-  in
-    cterm_instantiate (zip_options vs cts) thm
-  end;
-
 (*Returns t $ u, but instantiates the type of t to make the
 application type correct*)
 fun apply_inst ctxt t u =
@@ -168,13 +157,13 @@
   curry induction predicate *)
 fun specialize_fixp_induct ctxt args fT fT_uc F curry uncurry mono_thm f_def rule =
   let
-    val cert = Thm.cterm_of ctxt
     val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
     val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
   in 
     (* FIXME ctxt vs. ctxt' (!?) *)
     rule
-    |> cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry), NONE, SOME (cert P_inst)]
+    |> infer_instantiate' ctxt
+      ((map o Option.map) (Thm.cterm_of ctxt) [SOME uncurry, NONE, SOME curry, NONE, SOME P_inst])
     |> Tactic.rule_by_tactic ctxt
       (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 (* discharge U (C f) = f *)
        THEN Simplifier.simp_tac (put_simpset curry_K_ss ctxt) 4 (* simplify bot case *)
@@ -235,7 +224,6 @@
     val ((f_binding, fT), mixfix) = the_single fixes;
     val fname = Binding.name_of f_binding;
 
-    val cert = Thm.cterm_of lthy;
     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn);
     val (head, args) = strip_comb lhs;
     val argnames = map (fst o dest_Free) args;
@@ -258,9 +246,9 @@
       |> HOLogic.mk_Trueprop
       |> Logic.all x_uc;
 
-    val mono_thm = Goal.prove_internal lthy [] (cert mono_goal)
+    val mono_thm = Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal)
         (K (mono_tac lthy 1))
-    val inst_mono_thm = Thm.forall_elim (cert x_uc) mono_thm
+    val inst_mono_thm = Thm.forall_elim (Thm.cterm_of lthy x_uc) mono_thm
 
     val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
     val f_def_binding = Binding.concealed (Binding.name (Thm.def_name fname));
@@ -272,7 +260,7 @@
       |> HOLogic.mk_Trueprop;
 
     val unfold =
-      (cterm_instantiate' (map (SOME o cert) [uncurry, F, curry]) fixp_eq
+      (infer_instantiate' lthy' (map (SOME o Thm.cterm_of lthy') [uncurry, F, curry]) fixp_eq
         OF [inst_mono_thm, f_def])
       |> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1);
 
@@ -281,10 +269,12 @@
       |> Drule.rename_bvars' (map SOME (fname :: fname :: argnames));
 
     val mk_raw_induct =
-      cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry)]
+      infer_instantiate' args_ctxt
+        ((map o Option.map) (Thm.cterm_of args_ctxt) [SOME uncurry, NONE, SOME curry])
       #> mk_curried_induct args args_ctxt
       #> singleton (Variable.export args_ctxt lthy')
-      #> (fn thm => cterm_instantiate' [SOME (cert F)] thm OF [inst_mono_thm, f_def])
+      #> (fn thm => infer_instantiate' lthy'
+          [SOME (Thm.cterm_of lthy' F)] thm OF [inst_mono_thm, f_def])
       #> Drule.rename_bvars' (map SOME (fname :: argnames @ argnames))
 
     val raw_induct = Option.map mk_raw_induct fixp_induct_user
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -299,9 +299,11 @@
           THEN' (blast_tac ctxt)))    (* Solve rest of context... not very elegant *)
       ) i
   in
-    (PRIMITIVE (Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt) (rel, relation)])
-     THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
-     THEN rewrite_goal_tac ctxt Un_aci_simps 1)  (* eliminate duplicates *)
+    if is_Var rel then
+      PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)])
+        THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
+        THEN rewrite_goal_tac ctxt Un_aci_simps 1  (* eliminate duplicates *)
+    else no_tac
   end) 1 st
 
 end
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -183,19 +183,17 @@
         val param_rel = (snd o dest_comb o fst o dest_comb) tm;
         val free_vars = Term.add_vars param_rel [];
         
-        fun make_subst (var as (_, typ)) subst = 
+        fun make_subst (xi, typ) subst = 
           let
             val [rty, rty'] = binder_types typ
           in
-            if (Term.is_TVar rty andalso is_Type rty') then
-              (Var var, HOLogic.eq_const rty')::subst
+            if Term.is_TVar rty andalso is_Type rty' then
+              (xi, Thm.cterm_of ctxt (HOLogic.eq_const rty')) :: subst
             else
               subst
           end;
-        
-        val subst = fold make_subst free_vars [];
-        val csubst = map (apply2 (Thm.cterm_of ctxt)) subst;
-        val inst_thm = Drule.cterm_instantiate csubst thm;
+
+        val inst_thm = infer_instantiate ctxt (fold make_subst free_vars []) thm;
       in
         Conv.fconv_rule 
           ((Conv.concl_conv (Thm.nprems_of inst_thm) o
@@ -212,10 +210,9 @@
         val fun2 = Thm.cterm_of ctxt (strip_args 2 t2)
         val args2 = map (Thm.cterm_of ctxt) (get_args 1 t2)
         val relcomppI = Drule.incr_indexes2 ant1 ant2 @{thm relcomppI}
-        val vars = (rev (Term.add_vars (Thm.prop_of relcomppI) []))
-        val subst = map (apfst (Thm.cterm_of ctxt o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
+        val vars = map #1 (rev (Term.add_vars (Thm.prop_of relcomppI) []))
       in
-        Drule.cterm_instantiate subst relcomppI
+        infer_instantiate ctxt (vars ~~ ([fun1] @ args1 @ [fun2] @ args2)) relcomppI
       end
 
     fun zip_transfer_rules ctxt thm =
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -217,9 +217,9 @@
       (quot_thm, (lthy, rel_eq_onps))
   end;
 
-fun case_tac rule ctxt i st =
-  (Subgoal.FOCUS_PARAMS (fn {params, ...} => HEADGOAL(rtac ctxt
-    (Ctr_Sugar_Util.cterm_instantiate_pos [SOME (params |> hd |> snd)] rule))) ctxt i st);
+fun case_tac rule =
+  Subgoal.FOCUS_PARAMS (fn {context = ctxt, params, ...} =>
+    HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME (snd (hd params))] rule)));
 
 fun bundle_name_of_bundle_binding binding phi context  =
   Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi binding);
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -132,18 +132,17 @@
       
       fun make_inst var ctxt = 
         let 
-          val typ = (snd o relation_types o snd o dest_Var) var
+          val typ = snd (relation_types (#2 (dest_Var var)))
           val sort = Type.sort_of_atyp typ
           val (fresh_var, ctxt') = yield_singleton Variable.invent_types sort ctxt
-        in
-          (apply2 (Thm.cterm_of ctxt') (var, HOLogic.eq_const (TFree fresh_var)), ctxt')
-        end
+          val inst = (#1 (dest_Var var), Thm.cterm_of ctxt' (HOLogic.eq_const (TFree fresh_var)))
+        in (inst, ctxt') end
       
       val orig_lthy = lthy
       val (args_inst, lthy) = fold_map make_inst args lthy
       val pcr_cr_eq = 
         pcr_rel_def
-        |> Drule.cterm_instantiate args_inst    
+        |> infer_instantiate lthy args_inst
         |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv 
           (Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy))))
   in
@@ -403,9 +402,9 @@
          @{thm id_transfer}
         |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
         |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
-      val var = Var (hd (Term.add_vars (Thm.prop_of id_transfer) []))
-      val inst = [(Thm.cterm_of lthy var, Thm.cterm_of lthy parametrized_relator)]
-      val id_par_thm = Drule.cterm_instantiate inst id_transfer
+      val var = hd (Term.add_vars (Thm.prop_of id_transfer) [])
+      val inst = [(#1 var, Thm.cterm_of lthy parametrized_relator)]
+      val id_par_thm = infer_instantiate lthy inst id_transfer
     in
       Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
     end
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/coinduction.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -80,15 +80,14 @@
             |> Term.map_abs_vars (Variable.revert_fixed ctxt)
             |> fold_rev Term.absfree (names ~~ Ts)
             |> Thm.cterm_of ctxt;
-          val thm = Ctr_Sugar_Util.cterm_instantiate_pos [SOME phi] raw_thm;
+          val thm = infer_instantiate' ctxt [SOME phi] raw_thm;
           val e = length eqs;
           val p = length prems;
         in
           HEADGOAL (EVERY' [resolve_tac ctxt [thm],
             EVERY' (map (fn var =>
               resolve_tac ctxt
-                [Ctr_Sugar_Util.cterm_instantiate_pos
-                  [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
+                [infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
             if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
             else
               REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/inductive.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -639,11 +639,11 @@
       | _ => error
         ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique"));
     val inst =
-      map (fn v => apply2 (Thm.cterm_of ctxt') (Var v, Envir.subst_term subst (Var v)))
+      map (fn v => (fst v, Thm.cterm_of ctxt' (Envir.subst_term subst (Var v))))
         (Term.add_vars (lhs_of eq) []);
   in
-    Drule.cterm_instantiate inst eq
-    |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite ctxt)))
+    infer_instantiate ctxt' inst eq
+    |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite ctxt')))
     |> singleton (Variable.export ctxt' ctxt)
   end
 
diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/legacy_transfer.ML
--- a/src/HOL/Tools/legacy_transfer.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/legacy_transfer.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -130,7 +130,7 @@
       put_simpset HOL_ss ctxt5 addsimps (inj @ embed @ return)
       |> fold Simplifier.add_cong cong;
     val thm' = thm
-      |> Drule.cterm_instantiate (c_vars ~~ c_exprs')
+      |> infer_instantiate ctxt5 (map (#1 o dest_Var o Thm.term_of) c_vars ~~ c_exprs')
       |> fold_rev Thm.implies_intr (map Thm.cprop_of hyps)
       |> Simplifier.asm_full_simplify simpset
   in singleton (Variable.export ctxt5 ctxt1) thm' end;
diff -r 495bede1c4d9 -r 4f590c08fd5d src/Tools/cong_tac.ML
--- a/src/Tools/cong_tac.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/Tools/cong_tac.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -23,11 +23,11 @@
           val _ $ (_ $ (f' $ x') $ (g' $ y')) = Logic.strip_assums_concl (Thm.prop_of cong');
           val ps = Logic.strip_params (Thm.concl_of cong');
           val insts =
-            [(f', f), (g', g), (x', x), (y', y)]
-            |> map (fn (t, u) => apply2 (Thm.cterm_of ctxt) (Term.head_of t, fold_rev Term.abs ps u));
+            [(f', f), (g', g), (x', x), (y', y)] |> map (fn (t, u) =>
+              (#1 (dest_Var (head_of t)), Thm.cterm_of ctxt (fold_rev Term.abs ps u)));
         in
           fn st =>
-            compose_tac ctxt (false, Drule.cterm_instantiate insts cong', 2) i st
+            compose_tac ctxt (false, infer_instantiate ctxt insts cong', 2) i st
               handle THM _ => no_tac st
         end
     | _ => no_tac)
diff -r 495bede1c4d9 -r 4f590c08fd5d src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/Tools/induct.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -390,14 +390,12 @@
 
 fun prep_inst ctxt align tune (tm, ts) =
   let
-    fun prep_var (x, SOME t) =
+    fun prep_var (Var (x, xT), SOME t) =
           let
-            val cx = Thm.cterm_of ctxt x;
-            val xT = Thm.typ_of_cterm cx;
             val ct = Thm.cterm_of ctxt (tune t);
             val tT = Thm.typ_of_cterm ct;
           in
-            if Type.could_unify (tT, xT) then SOME (cx, ct)
+            if Type.could_unify (tT, xT) then SOME (x, ct)
             else error (Pretty.string_of (Pretty.block
              [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
               Syntax.pretty_term ctxt (Thm.term_of ct), Pretty.str " ::", Pretty.brk 1,
@@ -478,7 +476,7 @@
        else
          (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
            |> maps (prep_inst ctxt align_left I)
-           |> Drule.cterm_instantiate) r)
+           |> infer_instantiate ctxt) r)
       |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
       |> pair (Rule_Cases.get r);
 
@@ -557,7 +555,7 @@
 (* prepare rule *)
 
 fun rule_instance ctxt inst rule =
-  Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
+  infer_instantiate ctxt (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
 
 fun internalize ctxt k th =
   th |> Thm.permute_prems 0 k
@@ -658,10 +656,9 @@
       |> Thm.lift_rule (Thm.cterm_of ctxt prfx)
       |> `(Thm.prop_of #> Logic.strip_assums_concl)
       |-> (fn pred $ arg =>
-        Drule.cterm_instantiate
-          (map (apply2 (Thm.cterm_of ctxt))
-            [(Term.head_of pred, Logic.rlist_abs (xs, body)),
-             (Term.head_of arg, Logic.rlist_abs (xs, v))]));
+        infer_instantiate ctxt
+          [(#1 (dest_Var (head_of pred)), Thm.cterm_of ctxt (Logic.rlist_abs (xs, body))),
+           (#1 (dest_Var (head_of arg)), Thm.cterm_of ctxt (Logic.rlist_abs (xs, v)))]);
 
     fun goal_concl k xs (Const (@{const_name Pure.all}, _) $ Abs (a, T, B)) =
           goal_concl k ((a, T) :: xs) B
@@ -745,7 +742,7 @@
          else (align_left "Rule has fewer conclusions than arguments given"
             (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
           |> maps (prep_inst ctxt align_right (atomize_term ctxt))
-          |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
+          |> infer_instantiate ctxt) r |> pair (Rule_Cases.get r))
         |> mod_cases
         |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
 
@@ -828,7 +825,8 @@
   let
     fun inst_rule r =
       if null inst then `Rule_Cases.get r
-      else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
+      else
+        infer_instantiate ctxt (prep_inst ctxt align_right I (main_prop_of r, inst)) r
         |> pair (Rule_Cases.get r);
   in
     fn st =>