updated to infer_instantiate;
authorwenzelm
Sat Jul 25 23:41:53 2015 +0200 (2015-07-25)
changeset 607812da59cdf531c
parent 60780 7e2c8a63a8f8
child 60782 ba81f7c40e2a
updated to infer_instantiate;
tuned;
src/HOL/HOL.thy
src/HOL/Library/old_recdef.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Function/function_context_tree.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/pat_completeness.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/set_comprehension_pointfree.ML
src/Provers/splitter.ML
     1.1 --- a/src/HOL/HOL.thy	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -1190,15 +1190,6 @@
     1.4  
     1.5  simproc_setup let_simp ("Let x f") = \<open>
     1.6  let
     1.7 -  val (f_Let_unfold, x_Let_unfold) =
     1.8 -    let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
     1.9 -    in apply2 (Thm.cterm_of @{context}) (f, x) end
    1.10 -  val (f_Let_folded, x_Let_folded) =
    1.11 -    let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_folded}
    1.12 -    in apply2 (Thm.cterm_of @{context}) (f, x) end;
    1.13 -  val g_Let_folded =
    1.14 -    let val [(_ $ _ $ (g $ _))] = Thm.prems_of @{thm Let_folded}
    1.15 -    in Thm.cterm_of @{context} g end;
    1.16    fun count_loose (Bound i) k = if i >= k then 1 else 0
    1.17      | count_loose (s $ t) k = count_loose s k + count_loose t k
    1.18      | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
    1.19 @@ -1234,7 +1225,7 @@
    1.20                  if g aconv g' then
    1.21                    let
    1.22                      val rl =
    1.23 -                      cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
    1.24 +                      infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
    1.25                    in SOME (rl OF [fx_g]) end
    1.26                  else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
    1.27                  then NONE (*avoid identity conversion*)
    1.28 @@ -1243,10 +1234,10 @@
    1.29                      val g'x = abs_g' $ x;
    1.30                      val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
    1.31                      val rl =
    1.32 -                      @{thm Let_folded} |> cterm_instantiate
    1.33 -                        [(f_Let_folded, Thm.cterm_of ctxt f),
    1.34 -                         (x_Let_folded, cx),
    1.35 -                         (g_Let_folded, Thm.cterm_of ctxt abs_g')];
    1.36 +                      @{thm Let_folded} |> infer_instantiate ctxt
    1.37 +                        [(("f", 0), Thm.cterm_of ctxt f),
    1.38 +                         (("x", 0), cx),
    1.39 +                         (("g", 0), Thm.cterm_of ctxt abs_g')];
    1.40                    in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
    1.41                end
    1.42            | _ => NONE)
     2.1 --- a/src/HOL/Library/old_recdef.ML	Sat Jul 25 23:15:37 2015 +0200
     2.2 +++ b/src/HOL/Library/old_recdef.ML	Sat Jul 25 23:41:53 2015 +0200
     2.3 @@ -175,8 +175,7 @@
     2.4    val PROVE_HYP: thm -> thm -> thm
     2.5  
     2.6    val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
     2.7 -  val EXISTS: cterm * cterm -> thm -> thm
     2.8 -  val EXISTL: cterm list -> thm -> thm
     2.9 +  val EXISTS: Proof.context -> cterm * cterm -> thm -> thm
    2.10    val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm
    2.11  
    2.12    val EVEN_ORS: thm list -> thm list
    2.13 @@ -1199,29 +1198,11 @@
    2.14        handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
    2.15    end;
    2.16  
    2.17 -local
    2.18 -  val prop = Thm.prop_of exI
    2.19 -  val [P, x] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars prop)
    2.20 -in
    2.21 -fun EXISTS (template,witness) thm =
    2.22 +fun EXISTS ctxt (template,witness) thm =
    2.23    let val abstr = #2 (Dcterm.dest_comb template) in
    2.24 -    thm RS (cterm_instantiate [(P, abstr), (x, witness)] exI)
    2.25 +    thm RS (infer_instantiate ctxt [(("P", 0), abstr), (("x", 0), witness)] exI)
    2.26        handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
    2.27 -  end
    2.28 -end;
    2.29 -
    2.30 -(*----------------------------------------------------------------------------
    2.31 - *
    2.32 - *         A |- M
    2.33 - *   -------------------   [v_1,...,v_n]
    2.34 - *    A |- ?v1...v_n. M
    2.35 - *
    2.36 - *---------------------------------------------------------------------------*)
    2.37 -
    2.38 -fun EXISTL vlist th =
    2.39 -  fold_rev (fn v => fn thm => EXISTS(Dcterm.mk_exists(v,cconcl thm), v) thm)
    2.40 -           vlist th;
    2.41 -
    2.42 +  end;
    2.43  
    2.44  (*----------------------------------------------------------------------------
    2.45   *
    2.46 @@ -1238,7 +1219,7 @@
    2.47      fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
    2.48    in
    2.49      fold_rev (fn (b as (r1,r2)) => fn thm =>
    2.50 -        EXISTS(ex r2 (subst_free [b]
    2.51 +        EXISTS ctxt (ex r2 (subst_free [b]
    2.52                     (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
    2.53                thm)
    2.54         blist' th
    2.55 @@ -1453,13 +1434,7 @@
    2.56  
    2.57  fun PGEN ctxt tych a vstr th =
    2.58    let val a1 = tych a
    2.59 -      val vstr1 = tych vstr
    2.60 -  in
    2.61 -  Thm.forall_intr a1
    2.62 -     (if (is_Free vstr)
    2.63 -      then cterm_instantiate [(vstr1,a1)] th
    2.64 -      else VSTRUCT_ELIM ctxt tych a vstr th)
    2.65 -  end;
    2.66 +  in Thm.forall_intr a1 (VSTRUCT_ELIM ctxt tych a vstr th) end;
    2.67  
    2.68  
    2.69  (*---------------------------------------------------------------------------
    2.70 @@ -2243,7 +2218,7 @@
    2.71       val a = Free (aname, T)
    2.72       val v = Free (vname, T)
    2.73       val a_eq_v = HOLogic.mk_eq(a,v)
    2.74 -     val ex_th0 = Rules.EXISTS (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
    2.75 +     val ex_th0 = Rules.EXISTS ctxt (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
    2.76                             (Rules.REFL (tych a))
    2.77       val th0 = Rules.ASSUME (tych a_eq_v)
    2.78       val rows = map (fn x => ([x], (th0,[]))) pats
     3.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Jul 25 23:15:37 2015 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Jul 25 23:41:53 2015 +0200
     3.3 @@ -788,8 +788,8 @@
     3.4            (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
     3.5          val dist =
     3.6            Drule.export_without_context
     3.7 -            (cterm_instantiate
     3.8 -              [(Thm.global_cterm_of thy distinct_f, rep_const)] Old_Datatype.distinct_lemma);
     3.9 +            (infer_instantiate (Proof_Context.init_global thy)
    3.10 +              [(#1 (dest_Var distinct_f), rep_const)] Old_Datatype.distinct_lemma);
    3.11          val (thy', defs', eqns') = fold (make_constr_def tname T T')
    3.12            (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, [])
    3.13        in
    3.14 @@ -1058,24 +1058,27 @@
    3.15      val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule_lemma)));
    3.16      val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
    3.17        map (Free o apfst fst o dest_Var) Ps;
    3.18 -    val indrule_lemma' = cterm_instantiate
    3.19 -      (map (Thm.global_cterm_of thy8) Ps ~~ map (Thm.global_cterm_of thy8) frees) indrule_lemma;
    3.20  
    3.21      val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
    3.22  
    3.23      val dt_induct_prop = Old_Datatype_Prop.make_ind descr';
    3.24      val dt_induct = Goal.prove_global_future thy8 []
    3.25        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
    3.26 -      (fn {prems, context = ctxt} => EVERY
    3.27 -        [resolve_tac ctxt [indrule_lemma'] 1,
    3.28 -         (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
    3.29 -           Object_Logic.atomize_prems_tac ctxt) 1,
    3.30 -         EVERY (map (fn (prem, r) => (EVERY
    3.31 -           [REPEAT (eresolve_tac ctxt Abs_inverse_thms' 1),
    3.32 -            simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
    3.33 -            DEPTH_SOLVE_1
    3.34 -              (assume_tac ctxt 1 ORELSE resolve_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
    3.35 -                (prems ~~ constr_defs))]);
    3.36 +      (fn {prems, context = ctxt} =>
    3.37 +        let
    3.38 +          val indrule_lemma' = infer_instantiate ctxt
    3.39 +            (map (#1 o dest_Var) Ps ~~ map (Thm.cterm_of ctxt) frees) indrule_lemma;
    3.40 +        in
    3.41 +          EVERY [resolve_tac ctxt [indrule_lemma'] 1,
    3.42 +           (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
    3.43 +             Object_Logic.atomize_prems_tac ctxt) 1,
    3.44 +           EVERY (map (fn (prem, r) => (EVERY
    3.45 +             [REPEAT (eresolve_tac ctxt Abs_inverse_thms' 1),
    3.46 +              simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
    3.47 +              DEPTH_SOLVE_1
    3.48 +                (assume_tac ctxt 1 ORELSE resolve_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
    3.49 +                  (prems ~~ constr_defs))]
    3.50 +        end);
    3.51  
    3.52      val case_names_induct = Old_Datatype_Data.mk_case_names_induct descr'';
    3.53  
     4.1 --- a/src/HOL/Tools/Function/function_context_tree.ML	Sat Jul 25 23:15:37 2015 +0200
     4.2 +++ b/src/HOL/Tools/Function/function_context_tree.ML	Sat Jul 25 23:41:53 2015 +0200
     4.3 @@ -119,10 +119,10 @@
     4.4          val subst = Pattern.match thy (c, tt') (Vartab.empty, Vartab.empty)
     4.5          val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
     4.6          val inst =
     4.7 -          map (fn v => apply2 (Thm.cterm_of ctxt) (Var v, Envir.subst_term subst (Var v)))
     4.8 +          map (fn v => (#1 v, Thm.cterm_of ctxt (Envir.subst_term subst (Var v))))
     4.9              (Term.add_vars c [])
    4.10        in
    4.11 -        (cterm_instantiate inst r, dep, branches)
    4.12 +        (infer_instantiate ctxt inst r, dep, branches)
    4.13        end handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
    4.14    | find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
    4.15  
     5.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Sat Jul 25 23:15:37 2015 +0200
     5.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Sat Jul 25 23:41:53 2015 +0200
     5.3 @@ -201,7 +201,7 @@
     5.4    
     5.5          in (* 4: proof reconstruction *)
     5.6            st |>
     5.7 -          (PRIMITIVE (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (rel, relation)])
     5.8 +          (PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)])
     5.9              THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1))
    5.10              THEN (resolve_tac ctxt @{thms wf_empty} 1)
    5.11              THEN EVERY (map (prove_row_tac ctxt) clean_table))
     6.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Sat Jul 25 23:15:37 2015 +0200
     6.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Sat Jul 25 23:41:53 2015 +0200
     6.3 @@ -24,9 +24,9 @@
     6.4  fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var
     6.5  
     6.6  fun inst_case_thm ctxt x P thm =
     6.7 -  let val [Pv, xv] = Term.add_vars (Thm.prop_of thm) []
     6.8 +  let val [P_name, x_name] = Term.add_var_names (Thm.prop_of thm) []
     6.9    in
    6.10 -    thm |> cterm_instantiate (map (apply2 (Thm.cterm_of ctxt)) [(Var xv, x), (Var Pv, P)])
    6.11 +    thm |> infer_instantiate ctxt [(x_name, Thm.cterm_of ctxt x), (P_name, Thm.cterm_of ctxt P)]
    6.12    end
    6.13  
    6.14  fun invent_vars constr i =
     7.1 --- a/src/HOL/Tools/Meson/meson.ML	Sat Jul 25 23:15:37 2015 +0200
     7.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sat Jul 25 23:41:53 2015 +0200
     7.3 @@ -10,7 +10,6 @@
     7.4  sig
     7.5    val trace : bool Config.T
     7.6    val max_clauses : int Config.T
     7.7 -  val term_pair_of: indexname * (typ * 'a) -> term * 'a
     7.8    val first_order_resolve : Proof.context -> thm -> thm -> thm
     7.9    val size_of_subgoals: thm -> int
    7.10    val has_too_many_clauses: Proof.context -> term -> bool
    7.11 @@ -95,8 +94,6 @@
    7.12  
    7.13  (** First-order Resolution **)
    7.14  
    7.15 -fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
    7.16 -
    7.17  (*FIXME: currently does not "rename variables apart"*)
    7.18  fun first_order_resolve ctxt thA thB =
    7.19    (case
    7.20 @@ -107,8 +104,8 @@
    7.21            val tenv =
    7.22              Pattern.first_order_match thy (tmB, tmA)
    7.23                                            (Vartab.empty, Vartab.empty) |> snd
    7.24 -          val ct_pairs = map (apply2 (Thm.cterm_of ctxt) o term_pair_of) (Vartab.dest tenv)
    7.25 -      in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
    7.26 +          val insts = Vartab.fold (fn (xi, (_, t)) => cons (xi, Thm.cterm_of ctxt t)) tenv [];
    7.27 +      in  thA RS (infer_instantiate ctxt insts thB) end) () of
    7.28      SOME th => th
    7.29    | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
    7.30  
    7.31 @@ -616,10 +613,6 @@
    7.32    handle NO_F_PATTERN () => NONE
    7.33  
    7.34  val ext_cong_neq = @{thm ext_cong_neq}
    7.35 -val F_ext_cong_neq =
    7.36 -  Term.add_vars (Thm.prop_of @{thm ext_cong_neq}) []
    7.37 -  |> filter (fn ((s, _), _) => s = "F")
    7.38 -  |> the_single |> Var
    7.39  
    7.40  (* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
    7.41  fun cong_extensionalize_thm ctxt th =
    7.42 @@ -628,11 +621,8 @@
    7.43          $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
    7.44             $ (t as _ $ _) $ (u as _ $ _))) =>
    7.45      (case get_F_pattern T t u of
    7.46 -       SOME p =>
    7.47 -       let val inst = [apply2 (Thm.cterm_of ctxt) (F_ext_cong_neq, p)] in
    7.48 -         th RS cterm_instantiate inst ext_cong_neq
    7.49 -       end
    7.50 -     | NONE => th)
    7.51 +      SOME p => th RS infer_instantiate ctxt [(("F", 0), Thm.cterm_of ctxt p)] ext_cong_neq
    7.52 +    | NONE => th)
    7.53    | _ => th)
    7.54  
    7.55  (* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
     8.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Sat Jul 25 23:15:37 2015 +0200
     8.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sat Jul 25 23:41:53 2015 +0200
     8.3 @@ -94,10 +94,6 @@
     8.4    | is_quasi_lambda_free (Abs _) = false
     8.5    | is_quasi_lambda_free _ = true
     8.6  
     8.7 -val [f_B,g_B] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_B}));
     8.8 -val [g_C,f_C] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_C}));
     8.9 -val [f_S,g_S] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_S}));
    8.10 -
    8.11  (* FIXME: Requires more use of cterm constructors. *)
    8.12  fun abstract ctxt ct =
    8.13    let
    8.14 @@ -118,7 +114,8 @@
    8.15                 if Term.is_dependent rand then (*S*)
    8.16                   let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator))
    8.17                       val crand = Thm.cterm_of ctxt (Abs (x, xT, rand))
    8.18 -                     val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
    8.19 +                     val abs_S' =
    8.20 +                      infer_instantiate ctxt [(("f", 0), crator), (("g", 0), crand)] @{thm abs_S}
    8.21                       val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_S')
    8.22                   in
    8.23                     Thm.transitive abs_S' (Conv.binop_conv (abstract ctxt) rhs)
    8.24 @@ -126,7 +123,8 @@
    8.25                 else (*C*)
    8.26                   let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator))
    8.27                       val abs_C' =
    8.28 -                      cterm_instantiate [(f_C, crator), (g_C, Thm.cterm_of ctxt rand)] @{thm abs_C}
    8.29 +                      infer_instantiate ctxt [(("f", 0), crator), (("b", 0), Thm.cterm_of ctxt rand)]
    8.30 +                        @{thm abs_C}
    8.31                       val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_C')
    8.32                   in
    8.33                     Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv (abstract ctxt)) rhs)
    8.34 @@ -136,7 +134,8 @@
    8.35                 else (*B*)
    8.36                   let val crand = Thm.cterm_of ctxt (Abs (x, xT, rand))
    8.37                       val crator = Thm.cterm_of ctxt rator
    8.38 -                     val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
    8.39 +                     val abs_B' =
    8.40 +                      infer_instantiate ctxt [(("a", 0), crator), (("g", 0), crand)] @{thm abs_B}
    8.41                       val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_B')
    8.42                   in Thm.transitive abs_B' (Conv.arg_conv (abstract ctxt) rhs) end
    8.43              else makeK ()
     9.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Jul 25 23:15:37 2015 +0200
     9.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Jul 25 23:41:53 2015 +0200
     9.3 @@ -650,7 +650,7 @@
     9.4                   |> sort (cluster_ord
     9.5                            o apply2 (Meson_Clausify.cluster_of_zapped_var_name
     9.6                                        o fst o fst))
     9.7 -                 |> map (Meson.term_pair_of #> apply2 (Envir.subst_term_types tyenv))
     9.8 +                 |> map (fn (xi, (T, t)) => apply2 (Envir.subst_term_types tyenv) (Var (xi, T), t))
     9.9            val tysubst = tyenv |> Vartab.dest
    9.10          in (tysubst, tsubst) end
    9.11  
    10.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sat Jul 25 23:15:37 2015 +0200
    10.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sat Jul 25 23:41:53 2015 +0200
    10.3 @@ -248,10 +248,11 @@
    10.4      fun dt_constr_defs (((((_, (_, _, constrs)), tname), typedef: Typedef.info), T), constr_syntax)
    10.5          (thy, defs, eqns, rep_congs, dist_lemmas) =
    10.6        let
    10.7 +        val ctxt = Proof_Context.init_global thy;
    10.8          val _ $ (_ $ (cong_f $ _) $ _) = Thm.concl_of arg_cong;
    10.9 -        val rep_const = Thm.global_cterm_of thy (Const (#Rep_name (#1 typedef), T --> Univ_elT));
   10.10 -        val cong' = cterm_instantiate [(Thm.global_cterm_of thy cong_f, rep_const)] arg_cong;
   10.11 -        val dist = cterm_instantiate [(Thm.global_cterm_of thy distinct_f, rep_const)] distinct_lemma;
   10.12 +        val rep_const = Thm.cterm_of ctxt (Const (#Rep_name (#1 typedef), T --> Univ_elT));
   10.13 +        val cong' = infer_instantiate ctxt [(#1 (dest_Var cong_f), rep_const)] arg_cong;
   10.14 +        val dist = infer_instantiate ctxt [(#1 (dest_Var distinct_f), rep_const)] distinct_lemma;
   10.15          val (thy', defs', eqns', _) =
   10.16            fold (make_constr_def typedef T (length constrs))
   10.17              (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
   10.18 @@ -635,8 +636,6 @@
   10.19      val frees =
   10.20        if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))]
   10.21        else map (Free o apfst fst o dest_Var) Ps;
   10.22 -    val indrule_lemma' =
   10.23 -      cterm_instantiate (map (Thm.global_cterm_of thy6) Ps ~~ map (Thm.global_cterm_of thy6) frees) indrule_lemma;
   10.24  
   10.25      val dt_induct_prop = Old_Datatype_Prop.make_ind descr;
   10.26      val dt_induct =
   10.27 @@ -644,16 +643,22 @@
   10.28        (Logic.strip_imp_prems dt_induct_prop)
   10.29        (Logic.strip_imp_concl dt_induct_prop)
   10.30        (fn {context = ctxt, prems, ...} =>
   10.31 -        EVERY
   10.32 -          [resolve_tac ctxt [indrule_lemma'] 1,
   10.33 -           (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
   10.34 -              Object_Logic.atomize_prems_tac ctxt) 1,
   10.35 -           EVERY (map (fn (prem, r) => (EVERY
   10.36 -             [REPEAT (eresolve_tac ctxt Abs_inverse_thms 1),
   10.37 -              simp_tac (put_simpset HOL_basic_ss ctxt
   10.38 -                addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
   10.39 -              DEPTH_SOLVE_1 (ares_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
   10.40 -                  (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]);
   10.41 +        let
   10.42 +          val indrule_lemma' =
   10.43 +            infer_instantiate ctxt
   10.44 +              (map (#1 o dest_Var) Ps ~~ map (Thm.cterm_of ctxt) frees) indrule_lemma;
   10.45 +        in
   10.46 +          EVERY
   10.47 +            [resolve_tac ctxt [indrule_lemma'] 1,
   10.48 +             (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
   10.49 +                Object_Logic.atomize_prems_tac ctxt) 1,
   10.50 +             EVERY (map (fn (prem, r) => (EVERY
   10.51 +               [REPEAT (eresolve_tac ctxt Abs_inverse_thms 1),
   10.52 +                simp_tac (put_simpset HOL_basic_ss ctxt
   10.53 +                  addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
   10.54 +                DEPTH_SOLVE_1 (ares_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
   10.55 +                    (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]
   10.56 +        end);
   10.57  
   10.58      val ([(_, [dt_induct'])], thy7) =
   10.59        thy6
    11.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sat Jul 25 23:15:37 2015 +0200
    11.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sat Jul 25 23:41:53 2015 +0200
    11.3 @@ -147,8 +147,8 @@
    11.4        (ts ~~ ts') |> map_filter (fn (t, u) =>
    11.5          (case abstr (getP u) of
    11.6            NONE => NONE
    11.7 -        | SOME u' => SOME (apply2 (Thm.cterm_of ctxt) (t |> getP |> snd |> head_of, u'))));
    11.8 -    val indrule' = cterm_instantiate insts indrule;
    11.9 +        | SOME u' => SOME (t |> getP |> snd |> head_of |> dest_Var |> #1, Thm.cterm_of ctxt u')));
   11.10 +    val indrule' = infer_instantiate ctxt insts indrule;
   11.11    in resolve_tac ctxt [indrule'] i end);
   11.12  
   11.13  
   11.14 @@ -163,9 +163,9 @@
   11.15      val prem' = hd (Thm.prems_of exhaustion);
   11.16      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
   11.17      val exhaustion' =
   11.18 -      cterm_instantiate
   11.19 -        [apply2 (Thm.cterm_of ctxt)
   11.20 -          (head_of lhs, fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0))]
   11.21 +      infer_instantiate ctxt
   11.22 +        [(#1 (dest_Var (head_of lhs)),
   11.23 +          Thm.cterm_of ctxt (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))]
   11.24          exhaustion;
   11.25    in compose_tac ctxt (false, exhaustion', Thm.nprems_of exhaustion) i end);
   11.26  
    12.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sat Jul 25 23:15:37 2015 +0200
    12.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sat Jul 25 23:41:53 2015 +0200
    12.3 @@ -46,21 +46,24 @@
    12.4            Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
    12.5              Var (("P", 0), HOLogic.boolT));
    12.6          val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
    12.7 -        val insts' = map (Thm.global_cterm_of thy) induct_Ps ~~ map (Thm.global_cterm_of thy) insts;
    12.8 -        val induct' =
    12.9 -          refl RS
   12.10 -            (nth (Old_Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i
   12.11 -             RSN (2, rev_mp));
   12.12        in
   12.13          Goal.prove_sorry_global thy []
   12.14            (Logic.strip_imp_prems t)
   12.15            (Logic.strip_imp_concl t)
   12.16            (fn {context = ctxt, prems, ...} =>
   12.17 -            EVERY
   12.18 -              [resolve_tac ctxt [induct'] 1,
   12.19 -               REPEAT (resolve_tac ctxt [TrueI] 1),
   12.20 -               REPEAT ((resolve_tac ctxt [impI] 1) THEN (eresolve_tac ctxt prems 1)),
   12.21 -               REPEAT (resolve_tac ctxt [TrueI] 1)])
   12.22 +            let
   12.23 +              val insts' = map (#1 o dest_Var) induct_Ps ~~ map (Thm.cterm_of ctxt) insts;
   12.24 +              val induct' =
   12.25 +                refl RS
   12.26 +                  (nth (Old_Datatype_Aux.split_conj_thm (infer_instantiate ctxt insts' induct)) i
   12.27 +                   RSN (2, rev_mp));
   12.28 +            in
   12.29 +              EVERY
   12.30 +                [resolve_tac ctxt [induct'] 1,
   12.31 +                 REPEAT (resolve_tac ctxt [TrueI] 1),
   12.32 +                 REPEAT ((resolve_tac ctxt [impI] 1) THEN (eresolve_tac ctxt prems 1)),
   12.33 +                 REPEAT (resolve_tac ctxt [TrueI] 1)]
   12.34 +            end)
   12.35        end;
   12.36  
   12.37      val casedist_thms =
   12.38 @@ -206,16 +209,19 @@
   12.39          val insts =
   12.40            map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
   12.41              ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
   12.42 -        val induct' = induct
   12.43 -          |> cterm_instantiate
   12.44 -            (map (Thm.global_cterm_of thy1) induct_Ps ~~ map (Thm.global_cterm_of thy1) insts);
   12.45        in
   12.46          Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy1 [] []
   12.47            (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
   12.48            (fn {context = ctxt, ...} =>
   12.49 -            #1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
   12.50 -              (((resolve_tac ctxt [induct'] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
   12.51 -                  rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
   12.52 +            let
   12.53 +              val induct' =
   12.54 +                infer_instantiate ctxt
   12.55 +                  (map (#1 o dest_Var) induct_Ps ~~ map (Thm.cterm_of ctxt) insts) induct;
   12.56 +            in
   12.57 +              #1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
   12.58 +                (((resolve_tac ctxt [induct'] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
   12.59 +                    rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))
   12.60 +            end))
   12.61        end;
   12.62  
   12.63      val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
   12.64 @@ -380,15 +386,16 @@
   12.65      fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
   12.66        let
   12.67          val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.prems_of exhaustion)));
   12.68 +        val ctxt = Proof_Context.init_global thy;
   12.69          val exhaustion' = exhaustion
   12.70 -          |> cterm_instantiate [apply2 (Thm.global_cterm_of thy) (lhs, Free ("x", T))];
   12.71 -        fun tac ctxt =
   12.72 +          |> infer_instantiate ctxt [(#1 (dest_Var lhs), Thm.cterm_of ctxt (Free ("x", T)))];
   12.73 +        val tac =
   12.74            EVERY [resolve_tac ctxt [exhaustion'] 1,
   12.75              ALLGOALS (asm_simp_tac
   12.76                (put_simpset HOL_ss ctxt addsimps (dist_rewrites' @ inject @ case_thms')))];
   12.77        in
   12.78 -        (Goal.prove_sorry_global thy [] [] t1 (tac o #context),
   12.79 -         Goal.prove_sorry_global thy [] [] t2 (tac o #context))
   12.80 +        (Goal.prove_sorry_global thy [] [] t1 (K tac),
   12.81 +         Goal.prove_sorry_global thy [] [] t2 (K tac))
   12.82        end;
   12.83  
   12.84      val split_thm_pairs =
   12.85 @@ -451,13 +458,13 @@
   12.86          val Const (@{const_name Pure.imp}, _) $ tm $ _ = t;
   12.87          val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
   12.88          val nchotomy' = nchotomy RS spec;
   12.89 -        val [v] = Term.add_vars (Thm.concl_of nchotomy') [];
   12.90 -        val nchotomy'' =
   12.91 -          cterm_instantiate [apply2 (Thm.global_cterm_of thy) (Var v, Ma)] nchotomy';
   12.92 +        val [v] = Term.add_var_names (Thm.concl_of nchotomy') [];
   12.93        in
   12.94          Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   12.95            (fn {context = ctxt, prems, ...} =>
   12.96              let
   12.97 +              val nchotomy'' =
   12.98 +                infer_instantiate ctxt [(v, Thm.cterm_of ctxt Ma)] nchotomy';
   12.99                val simplify = asm_simp_tac (put_simpset HOL_ss ctxt addsimps (prems @ case_rewrites))
  12.100              in
  12.101                EVERY [
    13.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sat Jul 25 23:15:37 2015 +0200
    13.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sat Jul 25 23:41:53 2015 +0200
    13.3 @@ -141,9 +141,8 @@
    13.4      (intros'', (local_defs, thy'))
    13.5    end
    13.6  
    13.7 -fun introrulify thy ths = 
    13.8 +fun introrulify ctxt ths = 
    13.9    let
   13.10 -    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
   13.11      val ((_, ths'), ctxt') = Variable.import true ths ctxt
   13.12      fun introrulify' th =
   13.13        let
   13.14 @@ -158,8 +157,8 @@
   13.15            in
   13.16              (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
   13.17            end
   13.18 -        val x =
   13.19 -          (Thm.cterm_of ctxt' o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
   13.20 +        val Var (x, _) =
   13.21 +          (the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
   13.22              Logic.dest_implies o Thm.prop_of) @{thm exI}
   13.23          fun prove_introrule (index, (ps, introrule)) =
   13.24            let
   13.25 @@ -167,7 +166,7 @@
   13.26                THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1
   13.27                THEN (EVERY (map (fn y =>
   13.28                  resolve_tac ctxt'
   13.29 -                  [Drule.cterm_instantiate [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}] 1) ps))
   13.30 +                  [infer_instantiate ctxt' [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}] 1) ps))
   13.31                THEN REPEAT_DETERM (resolve_tac ctxt' @{thms conjI} 1 THEN assume_tac ctxt' 1)
   13.32                THEN TRY (assume_tac ctxt' 1)
   13.33            in
   13.34 @@ -205,7 +204,7 @@
   13.35        val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
   13.36        val intros =
   13.37          if forall is_pred_equation specs then 
   13.38 -          map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs))
   13.39 +          map (split_conjuncts_in_assms ctxt) (introrulify ctxt (map (rewrite ctxt) specs))
   13.40          else if forall (is_intro constname) specs then
   13.41            map (rewrite_intros ctxt) specs
   13.42          else
    14.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sat Jul 25 23:15:37 2015 +0200
    14.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sat Jul 25 23:41:53 2015 +0200
    14.3 @@ -105,15 +105,17 @@
    14.4          (map (fn ((((i, _), T), U), tname) =>
    14.5            make_pred i U T (mk_proj i is r) (Free (tname, T)))
    14.6              (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
    14.7 -    val inst = map (apply2 (Thm.cterm_of ctxt)) (map head_of (HOLogic.dest_conj
    14.8 -      (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
    14.9 +    val inst =
   14.10 +      map (#1 o dest_Var o head_of)
   14.11 +        (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~
   14.12 +      map (Thm.cterm_of ctxt) ps;
   14.13  
   14.14      val thm =
   14.15        Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl)
   14.16          (fn prems =>
   14.17             EVERY [
   14.18              rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
   14.19 -            resolve_tac ctxt [cterm_instantiate inst induct] 1,
   14.20 +            resolve_tac ctxt [infer_instantiate ctxt inst induct] 1,
   14.21              ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
   14.22              rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
   14.23              REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (fn i =>
   14.24 @@ -190,7 +192,7 @@
   14.25            (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
   14.26          (fn prems =>
   14.27             EVERY [
   14.28 -            resolve_tac ctxt [cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust] 1,
   14.29 +            resolve_tac ctxt [infer_instantiate ctxt [(#1 (dest_Var y), Thm.cterm_of ctxt y')] exhaust] 1,
   14.30              ALLGOALS (EVERY'
   14.31                [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
   14.32                 resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
    15.1 --- a/src/HOL/Tools/inductive_set.ML	Sat Jul 25 23:15:37 2015 +0200
    15.2 +++ b/src/HOL/Tools/inductive_set.ML	Sat Jul 25 23:41:53 2015 +0200
    15.3 @@ -223,12 +223,11 @@
    15.4            let
    15.5              val U = HOLogic.dest_setT (body_type T);
    15.6              val Ts = HOLogic.strip_ptupleT fs' U;
    15.7 -            (* FIXME: should cterm_instantiate increment indexes? *)
    15.8              val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
    15.9 -            val (arg_cong_f, _) = arg_cong' |> Thm.cprop_of |> Drule.strip_imp_concl |>
   15.10 -              Thm.dest_comb |> snd |> Drule.strip_comb |> snd |> hd |> Thm.dest_comb
   15.11 +            val (Var (arg_cong_f, _), _) = arg_cong' |> Thm.concl_of |>
   15.12 +              dest_comb |> snd |> strip_comb |> snd |> hd |> dest_comb;
   15.13            in
   15.14 -            thm' RS (Drule.cterm_instantiate [(arg_cong_f,
   15.15 +            thm' RS (infer_instantiate ctxt [(arg_cong_f,
   15.16                Thm.cterm_of ctxt (Abs ("P", Ts ---> HOLogic.boolT,
   15.17                  HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
   15.18                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
    16.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Jul 25 23:15:37 2015 +0200
    16.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Jul 25 23:41:53 2015 +0200
    16.3 @@ -495,9 +495,9 @@
    16.4  fun instantiate_arg_cong ctxt pred =
    16.5    let
    16.6      val arg_cong = Thm.incr_indexes (maxidx_of_term pred + 1) @{thm arg_cong}
    16.7 -    val f $ _ = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of arg_cong)))
    16.8 +    val (Var (f, _) $ _, _) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of arg_cong))
    16.9    in
   16.10 -    cterm_instantiate [(Thm.cterm_of ctxt f, Thm.cterm_of ctxt pred)] arg_cong
   16.11 +    infer_instantiate ctxt [(f, Thm.cterm_of ctxt pred)] arg_cong
   16.12    end;
   16.13  
   16.14  fun simproc ctxt redex =
    17.1 --- a/src/Provers/splitter.ML	Sat Jul 25 23:15:37 2015 +0200
    17.2 +++ b/src/Provers/splitter.ML	Sat Jul 25 23:41:53 2015 +0200
    17.3 @@ -317,9 +317,10 @@
    17.4      val (cntxt, u) = mk_cntxt t pos (T --> U);
    17.5      val trlift' = Thm.lift_rule (Thm.cprem_of state i)
    17.6        (Thm.rename_boundvars abs_lift u trlift);
    17.7 -    val (P, _) = strip_comb (fst (Logic.dest_equals
    17.8 -      (Logic.strip_assums_concl (Thm.prop_of trlift'))));
    17.9 -  in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] trlift' end;
   17.10 +    val (Var (P, _), _) =
   17.11 +      strip_comb (fst (Logic.dest_equals
   17.12 +        (Logic.strip_assums_concl (Thm.prop_of trlift'))));
   17.13 +  in infer_instantiate ctxt [(P, Thm.cterm_of ctxt (abss Ts cntxt))] trlift' end;
   17.14  
   17.15  
   17.16  (*************************************************************
   17.17 @@ -338,10 +339,11 @@
   17.18  fun inst_split ctxt Ts t tt thm TB state i =
   17.19    let
   17.20      val thm' = Thm.lift_rule (Thm.cprem_of state i) thm;
   17.21 -    val (P, _) = strip_comb (fst (Logic.dest_equals
   17.22 -      (Logic.strip_assums_concl (Thm.prop_of thm'))));
   17.23 +    val (Var (P, _), _) =
   17.24 +      strip_comb (fst (Logic.dest_equals
   17.25 +        (Logic.strip_assums_concl (Thm.prop_of thm'))));
   17.26      val cntxt = mk_cntxt_splitthm t tt TB;
   17.27 -  in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] thm' end;
   17.28 +  in infer_instantiate ctxt [(P, Thm.cterm_of ctxt (abss Ts cntxt))] thm' end;
   17.29  
   17.30  
   17.31  (*****************************************************************************