simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
authorwenzelm
Sun Jul 05 15:02:30 2015 +0200 (2015-07-05)
changeset 6064248dd1cefb4ae
parent 60641 f6e8293747fd
child 60643 9173467ec5b6
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
NEWS
src/Doc/Implementation/Logic.thy
src/Doc/Implementation/Proof.thy
src/HOL/Decision_Procs/approximation.ML
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Eisbach/eisbach_rule_insts.ML
src/HOL/Eisbach/match_method.ML
src/HOL/Import/import_rule.ML
src/HOL/Library/Old_SMT/old_smt_normalize.ML
src/HOL/Library/Old_SMT/old_smt_utils.ML
src/HOL/Library/Old_SMT/old_z3_proof_literals.ML
src/HOL/Library/Old_SMT/old_z3_proof_parser.ML
src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
src/HOL/Library/cconv.ML
src/HOL/Library/old_recdef.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Library/rewrite.ML
src/HOL/Matrix_LP/Compute_Oracle/linker.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Function/relation.ML
src/HOL/Tools/Lifting/lifting_bnf.ML
src/HOL/Tools/Lifting/lifting_term.ML
src/HOL/Tools/Lifting/lifting_util.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_util.ML
src/HOL/Tools/SMT/z3_replay_methods.ML
src/HOL/Tools/SMT/z3_replay_util.ML
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/coinduction.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/monomorph.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/record.ML
src/HOL/Tools/reification.ML
src/HOL/Tools/sat.ML
src/HOL/Tools/semiring_normalizer.ML
src/HOL/Tools/split_rule.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/hypsubst.ML
src/Pure/Isar/element.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/subgoal.ML
src/Pure/Proof/proof_checker.ML
src/Pure/Tools/rule_insts.ML
src/Pure/conjunction.ML
src/Pure/drule.ML
src/Pure/goal.ML
src/Pure/more_thm.ML
src/Pure/raw_simplifier.ML
src/Pure/thm.ML
src/Pure/variable.ML
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/coherent.ML
src/Tools/induct.ML
src/Tools/misc_legacy.ML
src/Tools/nbe.ML
src/ZF/Tools/cartprod.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/NEWS	Fri Jul 03 16:19:45 2015 +0200
     1.2 +++ b/NEWS	Sun Jul 05 15:02:30 2015 +0200
     1.3 @@ -234,6 +234,12 @@
     1.4  command. Minor INCOMPATIBILITY, use 'function' instead.
     1.5  
     1.6  
     1.7 +** ML **
     1.8 +
     1.9 +* Thm.instantiate (and derivatives) no longer require the LHS of the
    1.10 +instantiation to be certified: plain variables are given directly.
    1.11 +
    1.12 +
    1.13  
    1.14  New in Isabelle2015 (May 2015)
    1.15  ------------------------------
     2.1 --- a/src/Doc/Implementation/Logic.thy	Fri Jul 03 16:19:45 2015 +0200
     2.2 +++ b/src/Doc/Implementation/Logic.thy	Sun Jul 05 15:02:30 2015 +0200
     2.3 @@ -656,7 +656,8 @@
     2.4    @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
     2.5    @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
     2.6    @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
     2.7 -  @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
     2.8 +  @{index_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
     2.9 +  -> thm -> thm"} \\
    2.10    @{index_ML Thm.add_axiom: "Proof.context ->
    2.11    binding * term -> theory -> (string * thm) * theory"} \\
    2.12    @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
     3.1 --- a/src/Doc/Implementation/Proof.thy	Fri Jul 03 16:19:45 2015 +0200
     3.2 +++ b/src/Doc/Implementation/Proof.thy	Sun Jul 05 15:02:30 2015 +0200
     3.3 @@ -108,7 +108,7 @@
     3.4    @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
     3.5    @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
     3.6    @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
     3.7 -  (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\
     3.8 +  ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context"} \\
     3.9    @{index_ML Variable.focus: "term -> Proof.context ->
    3.10    ((string * (string * typ)) list * term) * Proof.context"} \\
    3.11    \end{mldecls}
     4.1 --- a/src/HOL/Decision_Procs/approximation.ML	Fri Jul 03 16:19:45 2015 +0200
     4.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Sun Jul 05 15:02:30 2015 +0200
     4.3 @@ -78,9 +78,9 @@
     4.4                 |> HOLogic.mk_list @{typ nat}
     4.5                 |> Thm.cterm_of ctxt
     4.6       in
     4.7 -       (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
     4.8 -                                   (@{cpat "?prec::nat"}, p),
     4.9 -                                   (@{cpat "?ss::nat list"}, s)])
    4.10 +       (rtac (Thm.instantiate ([], [((("n", 0), @{typ nat}), n),
    4.11 +                                   ((("prec", 0), @{typ nat}), p),
    4.12 +                                   ((("ss", 0), @{typ "nat list"}), s)])
    4.13              @{thm "approx_form"}) i
    4.14          THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st
    4.15       end
    4.16 @@ -95,9 +95,9 @@
    4.17         val s = vs |> map lookup_splitting |> hd
    4.18              |> Thm.cterm_of ctxt
    4.19       in
    4.20 -       rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s),
    4.21 -                                   (@{cpat "?t::nat"}, t),
    4.22 -                                   (@{cpat "?prec::nat"}, p)])
    4.23 +       rtac (Thm.instantiate ([], [((("s", 0), @{typ nat}), s),
    4.24 +                                   ((("t", 0), @{typ nat}), t),
    4.25 +                                   ((("prec", 0), @{typ nat}), p)])
    4.26              @{thm "approx_tse_form"}) i st
    4.27       end
    4.28    end
     5.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Jul 03 16:19:45 2015 +0200
     5.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Jul 05 15:02:30 2015 +0200
     5.3 @@ -58,6 +58,7 @@
     5.4     funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
     5.5       (funpow 4 Thm.dest_arg (Thm.cprop_of (hd minf)))
     5.6     |> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun)
     5.7 +   |> apply2 (apply2 (dest_Var o Thm.term_of))
     5.8  
     5.9   fun myfwd (th1, th2, th3, th4, th5) p1 p2
    5.10        [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] =
    5.11 @@ -73,7 +74,7 @@
    5.12    in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
    5.13        fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
    5.14    end
    5.15 - val U_v = (Thm.dest_arg o Thm.dest_arg o Thm.dest_arg1) (Thm.cprop_of qe)
    5.16 + val U_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 (Thm.cprop_of qe)))))
    5.17   fun main vs p =
    5.18    let
    5.19     val ((xn,ce),(x,fm)) = (case Thm.term_of p of
     6.1 --- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Fri Jul 03 16:19:45 2015 +0200
     6.2 +++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Sun Jul 05 15:02:30 2015 +0200
     6.3 @@ -57,7 +57,7 @@
     6.4  
     6.5      fun add_inst (xi, t) (Ts, ts) =
     6.6        (case AList.lookup (op =) tyvars xi of
     6.7 -        SOME S => ((certT (TVar (xi, S)), certT (Logic.dest_type t)) :: Ts, ts)
     6.8 +        SOME S => (((xi, S), certT (Logic.dest_type t)) :: Ts, ts)
     6.9        | NONE =>
    6.10            (case AList.lookup (op =) tvars xi of
    6.11              SOME T => (Ts, (cert (Var (xi, T)), cert t) :: ts)
     7.1 --- a/src/HOL/Eisbach/match_method.ML	Fri Jul 03 16:19:45 2015 +0200
     7.2 +++ b/src/HOL/Eisbach/match_method.ML	Sun Jul 05 15:02:30 2015 +0200
     7.3 @@ -440,10 +440,9 @@
     7.4  
     7.5  val focus_schematics = #2 o Focus_Data.get;
     7.6  
     7.7 -fun add_focus_schematics cterms =
     7.8 +fun add_focus_schematics schematics =
     7.9    (Focus_Data.map o @{apply 3(2)})
    7.10 -    (fold (fn (Var (xi, T), t) => Vartab.update_new (xi, (T, t)))
    7.11 -      (map (apply2 Thm.term_of) cterms));
    7.12 +    (fold (fn ((xi, T), ct) => Vartab.update_new (xi, (T, Thm.term_of ct))) schematics);
    7.13  
    7.14  
    7.15  (* focus params *)
     8.1 --- a/src/HOL/Import/import_rule.ML	Fri Jul 03 16:19:45 2015 +0200
     8.2 +++ b/src/HOL/Import/import_rule.ML	Sun Jul 05 15:02:30 2015 +0200
     8.3 @@ -161,11 +161,9 @@
     8.4    let
     8.5      val tvars = Term.add_tvars (Thm.prop_of thm) []
     8.6      val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars
     8.7 -    val tvars = map TVar tvars
     8.8      val thy = Thm.theory_of_thm thm
     8.9 -    fun inst ty = Thm.global_ctyp_of thy ty
    8.10    in
    8.11 -    Thm.instantiate ((map inst tvars ~~ map inst tfrees), []) thm
    8.12 +    Thm.instantiate ((tvars ~~ map (Thm.global_ctyp_of thy) tfrees), []) thm
    8.13    end
    8.14  
    8.15  fun def' constname rhs thy =
    8.16 @@ -264,11 +262,12 @@
    8.17      val tys_before = Term.add_tfrees (Thm.prop_of th) []
    8.18      val th1 = Thm.varifyT_global th
    8.19      val tys_after = Term.add_tvars (Thm.prop_of th1) []
    8.20 -    val tyinst = map2 (fn bef => fn iS =>
    8.21 -       (case try (assoc (TFree bef)) lambda of
    8.22 -              SOME cty => (Thm.global_ctyp_of thy (TVar iS), cty)
    8.23 -            | NONE => (Thm.global_ctyp_of thy (TVar iS), Thm.global_ctyp_of thy (TFree bef))
    8.24 -       )) tys_before tys_after
    8.25 +    val tyinst =
    8.26 +      map2 (fn bef => fn iS =>
    8.27 +        (case try (assoc (TFree bef)) lambda of
    8.28 +          SOME cty => (iS, cty)
    8.29 +        | NONE => (iS, Thm.global_ctyp_of thy (TFree bef))))
    8.30 +      tys_before tys_after
    8.31    in
    8.32      Thm.instantiate (tyinst,[]) th1
    8.33    end
    8.34 @@ -334,9 +333,7 @@
    8.35      val tns = map (fn (_, _) => "'") tvs
    8.36      val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
    8.37      val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
    8.38 -    val cvs = map (Thm.ctyp_of ctxt) vs
    8.39 -    val ctvs = map (Thm.ctyp_of ctxt) (map TVar tvs)
    8.40 -    val thm' = Thm.instantiate ((ctvs ~~ cvs), []) thm
    8.41 +    val thm' = Thm.instantiate ((tvs ~~ map (Thm.ctyp_of ctxt) vs), []) thm
    8.42    in
    8.43      snd (Global_Theory.add_thm ((binding, thm'), []) thy)
    8.44    end
     9.1 --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Fri Jul 03 16:19:45 2015 +0200
     9.2 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Sun Jul 05 15:02:30 2015 +0200
     9.3 @@ -34,7 +34,7 @@
     9.4  
     9.5    fun inst f ct thm =
     9.6      let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
     9.7 -    in Thm.instantiate ([], [(cv, ct)]) thm end
     9.8 +    in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end
     9.9  in
    9.10  
    9.11  fun instantiate_elim thm =
    9.12 @@ -215,7 +215,7 @@
    9.13    fun insert_trigger_conv [] ct = Conv.all_conv ct
    9.14      | insert_trigger_conv ctss ct =
    9.15          let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
    9.16 -        in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end
    9.17 +        in Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]) trigger_eq end
    9.18  
    9.19    fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
    9.20      let
    9.21 @@ -298,7 +298,8 @@
    9.22    fun mk_weight_eq w =
    9.23      let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq)
    9.24      in
    9.25 -      Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq
    9.26 +      Thm.instantiate ([], [(dest_Var (Thm.term_of cv), Numeral.mk_cnumber @{ctyp int} w)])
    9.27 +        weight_eq
    9.28      end
    9.29  
    9.30    fun add_weight_conv NONE _ = Conv.all_conv
    10.1 --- a/src/HOL/Library/Old_SMT/old_smt_utils.ML	Fri Jul 03 16:19:45 2015 +0200
    10.2 +++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML	Sun Jul 05 15:02:30 2015 +0200
    10.3 @@ -152,7 +152,7 @@
    10.4  val destT1 = hd o Thm.dest_ctyp
    10.5  val destT2 = hd o tl o Thm.dest_ctyp
    10.6  
    10.7 -fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
    10.8 +fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct
    10.9  fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
   10.10  fun instT' ct = instT (Thm.ctyp_of_cterm ct)
   10.11  
    11.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML	Fri Jul 03 16:19:45 2015 +0200
    11.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML	Sun Jul 05 15:02:30 2015 +0200
    11.3 @@ -195,7 +195,9 @@
    11.4    fun on_cprop f thm = f (Thm.cprop_of thm)
    11.5    fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm)
    11.6    fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
    11.7 -    Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
    11.8 +    Thm.instantiate ([],
    11.9 +      [(dest_Var (Thm.term_of cv1), on_cprop f thm1),
   11.10 +       (dest_Var (Thm.term_of cv2), on_cprop g thm2)]) rule
   11.11      |> Old_Z3_Proof_Tools.discharge thm1 |> Old_Z3_Proof_Tools.discharge thm2
   11.12  
   11.13    fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)
   11.14 @@ -303,7 +305,7 @@
   11.15            |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
   11.16      end
   11.17  
   11.18 -  val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))
   11.19 +  val falseE_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))))
   11.20    fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
   11.21  in
   11.22  fun contradict conj ct =
    12.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML	Fri Jul 03 16:19:45 2015 +0200
    12.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML	Sun Jul 05 15:02:30 2015 +0200
    12.3 @@ -109,7 +109,7 @@
    12.4      val max = fold (Integer.max o fst) vars 0
    12.5      val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
    12.6      fun mk (i, v) =
    12.7 -      (v, Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
    12.8 +      (dest_Var (Thm.term_of v), Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
    12.9    in map mk vars end
   12.10  
   12.11  fun close ctxt (ct, vars) =
   12.12 @@ -161,7 +161,10 @@
   12.13          if null vars then ([], vars)
   12.14          else fold part vars ([], [])
   12.15  
   12.16 -    in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end
   12.17 +    in
   12.18 +      (Thm.instantiate_cterm ([], map (apfst (dest_Var o Thm.term_of)) inst) ct,
   12.19 +        (maxidx', vars' @ all_vars))
   12.20 +    end
   12.21  in
   12.22  fun mk_fun f ts =
   12.23    let val (cts, (_, vars)) = fold_map prep ts (0, [])
    13.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Fri Jul 03 16:19:45 2015 +0200
    13.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sun Jul 05 15:02:30 2015 +0200
    13.3 @@ -625,7 +625,10 @@
    13.4        val vs = frees_of ctxt (Thm.term_of ct)
    13.5        val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt
    13.6        val vars_of = get_vars Term.add_vars Var (K true) ctxt'
    13.7 -    in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
    13.8 +    in
    13.9 +      (Thm.instantiate ([], map (dest_Var o Thm.term_of) (vars_of (Thm.prop_of thm)) ~~ vs) thm,
   13.10 +        ctxt')
   13.11 +    end
   13.12  
   13.13    val sk_rules = @{lemma
   13.14      "c = (SOME x. P x) ==> (EX x. P x) = P c"
    14.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Fri Jul 03 16:19:45 2015 +0200
    14.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Sun Jul 05 15:02:30 2015 +0200
    14.3 @@ -27,7 +27,7 @@
    14.4      (Proof.context -> cterm -> thm) -> cterm -> thm
    14.5  
    14.6    (*a faster COMP*)
    14.7 -  type compose_data
    14.8 +  type compose_data = cterm list * (cterm -> cterm list) * thm
    14.9    val precompose: (cterm -> cterm list) -> thm -> compose_data
   14.10    val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
   14.11    val compose: compose_data -> thm -> thm
   14.12 @@ -257,11 +257,11 @@
   14.13  
   14.14  fun list2 (x, y) = [x, y]
   14.15  
   14.16 -fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
   14.17 -fun precompose2 f rule = precompose (list2 o f) rule
   14.18 +fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule)
   14.19 +fun precompose2 f rule : compose_data = precompose (list2 o f) rule
   14.20  
   14.21  fun compose (cvs, f, rule) thm =
   14.22 -  discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
   14.23 +  discharge thm (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
   14.24  
   14.25  
   14.26  
    15.1 --- a/src/HOL/Library/cconv.ML	Fri Jul 03 16:19:45 2015 +0200
    15.2 +++ b/src/HOL/Library/cconv.ML	Sun Jul 05 15:02:30 2015 +0200
    15.3 @@ -182,7 +182,7 @@
    15.4            ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
    15.5        | _ =>  cv ct)
    15.6  
    15.7 -fun inst_imp_cong ct = Thm.instantiate ([], [(@{cpat "?A :: prop"}, ct)]) Drule.imp_cong
    15.8 +fun inst_imp_cong ct = Thm.instantiate ([], [((("A", 0), propT), ct)]) Drule.imp_cong
    15.9  
   15.10  (*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
   15.11  fun concl_cconv 0 cv ct = cv ct
   15.12 @@ -202,10 +202,10 @@
   15.13              NONE => (As, B)
   15.14            | SOME (A,B) => strip_prems (i - 1) (A::As) B
   15.15      val (prem, (prems, concl)) = ct |> Thm.dest_implies ||> strip_prems n [] 
   15.16 -    val rewr_imp_concl = Thm.instantiate ([], [(@{cpat "?C :: prop"}, concl)]) @{thm rewr_imp}
   15.17 +    val rewr_imp_concl = Thm.instantiate ([], [((("C", 0), propT), concl)]) @{thm rewr_imp}
   15.18      val th1 = cv prem RS rewr_imp_concl
   15.19      val nprems = Thm.nprems_of th1
   15.20 -    fun inst_cut_rl ct = Thm.instantiate ([], [(@{cpat "?psi :: prop"}, ct)]) cut_rl
   15.21 +    fun inst_cut_rl ct = Thm.instantiate ([], [((("psi", 0), propT), ct)]) cut_rl
   15.22      fun f p th = (th RS inst_cut_rl p)
   15.23        |> Conv.fconv_rule (Conv.concl_conv nprems (Conv.rewr_conv @{thm imp_cong_eq}))
   15.24    in fold f prems th1 end
    16.1 --- a/src/HOL/Library/old_recdef.ML	Fri Jul 03 16:19:45 2015 +0200
    16.2 +++ b/src/HOL/Library/old_recdef.ML	Sun Jul 05 15:02:30 2015 +0200
    16.3 @@ -304,15 +304,15 @@
    16.4              (Pv, Dv,
    16.5               Sign.typ_match thy (Dty, ty) Vartab.empty)
    16.6            | _ => error "not a valid case thm";
    16.7 -      val type_cinsts = map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T))
    16.8 +      val type_cinsts = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T))
    16.9          (Vartab.dest type_insts);
   16.10 -      val cPv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Pv);
   16.11 -      val cDv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Dv);
   16.12 +      val Pv = dest_Var (Envir.subst_term_types type_insts Pv);
   16.13 +      val Dv = dest_Var (Envir.subst_term_types type_insts Dv);
   16.14      in
   16.15        Conv.fconv_rule Drule.beta_eta_conversion
   16.16           (case_thm
   16.17              |> Thm.instantiate (type_cinsts, [])
   16.18 -            |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)]))
   16.19 +            |> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)]))
   16.20      end;
   16.21  
   16.22  
   16.23 @@ -1124,11 +1124,11 @@
   16.24  local (* this is fragile *)
   16.25    val prop = Thm.prop_of spec
   16.26    val x = hd (tl (Misc_Legacy.term_vars prop))
   16.27 -  val cTV = Thm.ctyp_of @{context} (type_of x)
   16.28 +  val TV = dest_TVar (type_of x)
   16.29    val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec
   16.30  in
   16.31  fun SPEC tm thm =
   16.32 -   let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_cterm tm)], []) gspec
   16.33 +   let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec
   16.34     in thm RS (Thm.forall_elim tm gspec') end
   16.35  end;
   16.36  
   16.37 @@ -1141,11 +1141,11 @@
   16.38  local
   16.39    val prop = Thm.prop_of allI
   16.40    val [P] = Misc_Legacy.add_term_vars (prop, [])
   16.41 -  fun cty_theta ctxt = map (fn (i, (S, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (i, S), ty))
   16.42 +  fun cty_theta ctxt = map (fn (i, (S, ty)) => ((i, S), Thm.ctyp_of ctxt ty))
   16.43    fun ctm_theta ctxt =
   16.44      map (fn (i, (_, tm2)) =>
   16.45        let val ctm2 = Thm.cterm_of ctxt tm2
   16.46 -      in (Thm.cterm_of ctxt (Var (i, Thm.typ_of_cterm ctm2)), ctm2) end)
   16.47 +      in ((i, Thm.typ_of_cterm ctm2), ctm2) end)
   16.48    fun certify ctxt (ty_theta,tm_theta) =
   16.49      (cty_theta ctxt (Vartab.dest ty_theta),
   16.50       ctm_theta ctxt (Vartab.dest tm_theta))
    17.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri Jul 03 16:19:45 2015 +0200
    17.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sun Jul 05 15:02:30 2015 +0200
    17.3 @@ -483,7 +483,7 @@
    17.4      fun real_not_eq_conv ct =
    17.5        let
    17.6          val (l,r) = dest_eq (Thm.dest_arg ct)
    17.7 -        val th = Thm.instantiate ([],[(@{cpat "?x::real"},l),(@{cpat "?y::real"},r)]) neq_th
    17.8 +        val th = Thm.instantiate ([],[((("x", 0), @{typ real}),l),((("y", 0), @{typ real}),r)]) neq_th
    17.9          val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
   17.10          val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
   17.11          val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
   17.12 @@ -729,9 +729,9 @@
   17.13        val pth_max = instantiate' [SOME @{ctyp real}] [] max_split
   17.14        val pth_min = instantiate' [SOME @{ctyp real}] [] min_split
   17.15        val abs_tm = @{cterm "abs :: real => _"}
   17.16 -      val p_tm = @{cpat "?P :: real => bool"}
   17.17 -      val x_tm = @{cpat "?x :: real"}
   17.18 -      val y_tm = @{cpat "?y::real"}
   17.19 +      val p_v = (("P", 0), @{typ "real \<Rightarrow> bool"})
   17.20 +      val x_v = (("x", 0), @{typ real})
   17.21 +      val y_v = (("y", 0), @{typ real})
   17.22        val is_max = is_binop @{cterm "max :: real => _"}
   17.23        val is_min = is_binop @{cterm "min :: real => _"}
   17.24        fun is_abs t = is_comb t andalso Thm.dest_fun t aconvc abs_tm
   17.25 @@ -746,16 +746,16 @@
   17.26  
   17.27        val elim_abs = eliminate_construct is_abs
   17.28          (fn p => fn ax =>
   17.29 -          Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax)]) pth_abs)
   17.30 +          Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax)]) pth_abs)
   17.31        val elim_max = eliminate_construct is_max
   17.32          (fn p => fn ax =>
   17.33            let val (ax,y) = Thm.dest_comb ax
   17.34 -          in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)])
   17.35 +          in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)])
   17.36                               pth_max end)
   17.37        val elim_min = eliminate_construct is_min
   17.38          (fn p => fn ax =>
   17.39            let val (ax,y) = Thm.dest_comb ax
   17.40 -          in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)])
   17.41 +          in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)])
   17.42                               pth_min end)
   17.43      in first_conv [elim_abs, elim_max, elim_min, all_conv]
   17.44      end;
    18.1 --- a/src/HOL/Library/rewrite.ML	Fri Jul 03 16:19:45 2015 +0200
    18.2 +++ b/src/HOL/Library/rewrite.ML	Sun Jul 05 15:02:30 2015 +0200
    18.3 @@ -265,15 +265,13 @@
    18.4    let
    18.5      fun instantiate_normalize_env ctxt env thm =
    18.6        let
    18.7 -        fun certs f = map (apply2 (f ctxt))
    18.8          val prop = Thm.prop_of thm
    18.9          val norm_type = Envir.norm_type o Envir.type_env
   18.10          val insts = Term.add_vars prop []
   18.11 -          |> map (fn x as (s,T) => (Var (s, norm_type env T), Envir.norm_term env (Var x)))
   18.12 -          |> certs Thm.cterm_of
   18.13 +          |> map (fn x as (s, T) =>
   18.14 +              ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x))))
   18.15          val tyinsts = Term.add_tvars prop []
   18.16 -          |> map (fn x => (TVar x, norm_type env (TVar x)))
   18.17 -          |> certs Thm.ctyp_of
   18.18 +          |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x))))
   18.19        in Drule.instantiate_normalize (tyinsts, insts) thm end
   18.20      
   18.21      fun unify_with_rhs context to env thm =
    19.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML	Fri Jul 03 16:19:45 2015 +0200
    19.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML	Sun Jul 05 15:02:30 2015 +0200
    19.3 @@ -315,8 +315,8 @@
    19.4      end
    19.5  
    19.6  fun conv_subst thy (subst : Type.tyenv) =
    19.7 -    map (fn (iname, (sort, ty)) => (Thm.global_ctyp_of thy (TVar (iname, sort)), Thm.global_ctyp_of thy ty))
    19.8 -      (Vartab.dest subst)
    19.9 +  map (fn (iname, (sort, ty)) => ((iname, sort), Thm.global_ctyp_of thy ty))
   19.10 +    (Vartab.dest subst)
   19.11  
   19.12  fun add_monos thy monocs pats ths =
   19.13      let
    20.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Fri Jul 03 16:19:45 2015 +0200
    20.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Sun Jul 05 15:02:30 2015 +0200
    20.3 @@ -258,8 +258,9 @@
    20.4  
    20.5  local
    20.6   val pth_zero = @{thm norm_zero}
    20.7 - val tv_n = (Thm.ctyp_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
    20.8 -             pth_zero
    20.9 + val tv_n =
   20.10 +  (dest_TVar o Thm.typ_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
   20.11 +    pth_zero
   20.12   val concl = Thm.dest_arg o Thm.cprop_of
   20.13   fun real_vector_combo_prover ctxt translator (nubs,ges,gts) =
   20.14    let
   20.15 @@ -356,7 +357,7 @@
   20.16    val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (#hyps (Thm.crep_thm th1))
   20.17    val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
   20.18    val cps = map (swap o Thm.dest_equals) (cprems_of th11)
   20.19 -  val th12 = Drule.instantiate_normalize ([], cps) th11
   20.20 +  val th12 = Drule.instantiate_normalize ([], map (apfst (dest_Var o Thm.term_of)) cps) th11
   20.21    val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
   20.22   in hd (Variable.export ctxt' ctxt [th13])
   20.23   end
    21.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Jul 03 16:19:45 2015 +0200
    21.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Jul 05 15:02:30 2015 +0200
    21.3 @@ -1390,13 +1390,13 @@
    21.4        end);
    21.5  
    21.6      val induct_aux' = Thm.instantiate ([],
    21.7 -      map (fn (s, v as Var (_, T)) =>
    21.8 -        (Thm.global_cterm_of thy9 v, Thm.global_cterm_of thy9 (Free (s, T))))
    21.9 +      map (fn (s, Var (v as (_, T))) =>
   21.10 +        (v, Thm.global_cterm_of thy9 (Free (s, T))))
   21.11            (pnames ~~ map head_of (HOLogic.dest_conj
   21.12               (HOLogic.dest_Trueprop (Thm.concl_of induct_aux)))) @
   21.13        map (fn (_, f) =>
   21.14          let val f' = Logic.varify_global f
   21.15 -        in (Thm.global_cterm_of thy9 f',
   21.16 +        in (dest_Var f',
   21.17            Thm.global_cterm_of thy9 (Const (@{const_name Nominal.supp}, fastype_of f')))
   21.18          end) fresh_fs) induct_aux;
   21.19  
   21.20 @@ -1562,7 +1562,7 @@
   21.21              (augment_sort thy1 pt_cp_sort
   21.22                (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
   21.23              (fn {context = ctxt, ...} => dtac (Thm.instantiate ([],
   21.24 -                 [(Thm.global_cterm_of thy11 (Var (("pi", 0), permT)),
   21.25 +                 [((("pi", 0), permT),
   21.26                     Thm.global_cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN
   21.27                 NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths)
   21.28        in (ths, ths') end) dt_atomTs);
   21.29 @@ -1653,7 +1653,7 @@
   21.30                      SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY
   21.31                        [cut_facts_tac [rec_prem] 1,
   21.32                         rtac (Thm.instantiate ([],
   21.33 -                         [(Thm.global_cterm_of thy11 (Var (("pi", 0), mk_permT aT)),
   21.34 +                         [((("pi", 0), mk_permT aT),
   21.35                             Thm.global_cterm_of thy11
   21.36                              (perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th) 1,
   21.37                         asm_simp_tac (put_simpset HOL_ss context addsimps
   21.38 @@ -1872,8 +1872,7 @@
   21.39                              val l = find_index (equal T) dt_atomTs;
   21.40                              val th = nth (nth rec_equiv_thms' l) k;
   21.41                              val th' = Thm.instantiate ([],
   21.42 -                              [(Thm.global_cterm_of thy11 (Var (("pi", 0), U)),
   21.43 -                                Thm.global_cterm_of thy11 p)]) th;
   21.44 +                              [((("pi", 0), U), Thm.global_cterm_of thy11 p)]) th;
   21.45                            in rtac th' 1 end;
   21.46                          val th' = Goal.prove context'' [] []
   21.47                            (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y))
    22.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Jul 03 16:19:45 2015 +0200
    22.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sun Jul 05 15:02:30 2015 +0200
    22.3 @@ -31,7 +31,10 @@
    22.4  (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
    22.5  
    22.6  fun res_inst_tac_term ctxt =
    22.7 -  gen_res_inst_tac_term ctxt (curry Thm.instantiate);
    22.8 +  gen_res_inst_tac_term ctxt (fn instT => fn inst =>
    22.9 +    Thm.instantiate
   22.10 +     (map (apfst (dest_TVar o Thm.typ_of)) instT,
   22.11 +      map (apfst (dest_Var o Thm.term_of)) inst));
   22.12  
   22.13  fun res_inst_tac_term' ctxt =
   22.14    gen_res_inst_tac_term ctxt (K Drule.cterm_instantiate) [];
   22.15 @@ -146,10 +149,10 @@
   22.16      fun inst_fresh vars params i st =
   22.17     let val vars' = Misc_Legacy.term_vars (Thm.prop_of st);
   22.18     in case subtract (op =) vars vars' of
   22.19 -     [x] =>
   22.20 +     [Var v] =>
   22.21        Seq.single
   22.22          (Thm.instantiate ([],
   22.23 -          [apply2 (Thm.cterm_of ctxt) (x, fold_rev Term.abs params (Bound 0))]) st)
   22.24 +          [(v, Thm.cterm_of ctxt (fold_rev Term.abs params (Bound 0)))]) st)
   22.25      | _ => error "fresh_fun_simp: Too many variables, please report."
   22.26     end
   22.27    in
    23.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 03 16:19:45 2015 +0200
    23.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 05 15:02:30 2015 +0200
    23.3 @@ -338,7 +338,8 @@
    23.4                   val pis'' = fold (concat_perm #> map) pis' pis;
    23.5                   val env = Pattern.first_order_match thy (ihypt, Thm.prop_of ihyp)
    23.6                     (Vartab.empty, Vartab.empty);
    23.7 -                 val ihyp' = Thm.instantiate ([], map (apply2 (Thm.global_cterm_of thy))
    23.8 +                 val ihyp' = Thm.instantiate ([],
    23.9 +                   map (fn (v, t) => (dest_Var v, Thm.global_cterm_of thy t))
   23.10                     (map (Envir.subst_term env) vs ~~
   23.11                      map (fold_rev (NominalDatatype.mk_perm [])
   23.12                        (rev pis' @ pis)) params' @ [z])) ihyp;
    24.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 03 16:19:45 2015 +0200
    24.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Jul 05 15:02:30 2015 +0200
    24.3 @@ -146,9 +146,7 @@
    24.4  fun inst_params thy (vs, p) th cts =
    24.5    let val env = Pattern.first_order_match thy (p, Thm.prop_of th)
    24.6      (Vartab.empty, Vartab.empty)
    24.7 -  in Thm.instantiate ([],
    24.8 -    map (Envir.subst_term env #> Thm.global_cterm_of thy) vs ~~ cts) th
    24.9 -  end;
   24.10 +  in Thm.instantiate ([], map (dest_Var o Envir.subst_term env) vs ~~ cts) th end;
   24.11  
   24.12  fun prove_strong_ind s alt_name avoids ctxt =
   24.13    let
    25.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Fri Jul 03 16:19:45 2015 +0200
    25.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Sun Jul 05 15:02:30 2015 +0200
    25.3 @@ -95,7 +95,11 @@
    25.4      fun mapT_and_recertify ct =
    25.5        (Thm.cterm_of ctxt (Term.map_types (Term.map_type_tvar substT) (Thm.term_of ct)));
    25.6      val insts' = map (apfst mapT_and_recertify) insts;
    25.7 -  in Thm.instantiate (instTs, insts') end;
    25.8 +  in
    25.9 +    Thm.instantiate
   25.10 +     (map (apfst (dest_TVar o Thm.typ_of)) instTs,
   25.11 +      map (apfst (dest_Var o Thm.term_of)) insts')
   25.12 +  end;
   25.13  
   25.14  fun tvar_clash ixn S S' =
   25.15    raise TYPE ("Type variable has two distinct sorts", [TVar (ixn, S), TVar (ixn, S')], []);
   25.16 @@ -145,9 +149,9 @@
   25.17      val (tyinsts,insts) =
   25.18        fold naive_cterm_first_order_match (Thm.prems_of rule ~~ map Thm.cprop_of prems) ([], []);
   25.19      val tyinsts' =
   25.20 -      map (fn (v, (S, U)) => apply2 (Thm.ctyp_of ctxt) (TVar (v, S), U)) tyinsts;
   25.21 +      map (fn (v, (S, U)) => ((v, S), Thm.ctyp_of ctxt U)) tyinsts;
   25.22      val insts' =
   25.23 -      map (fn (idxn, ct) => (Thm.cterm_of ctxt (Var (idxn, Thm.typ_of_cterm ct)), ct)) insts;
   25.24 +      map (fn (idxn, ct) => ((idxn, Thm.typ_of_cterm ct), ct)) insts;
   25.25      val rule' = Thm.instantiate (tyinsts', insts') rule;
   25.26    in fold Thm.elim_implies prems rule' end;
   25.27  
   25.28 @@ -286,7 +290,7 @@
   25.29          @{thm subtract_Tip} |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   25.30          |> Thm.dest_comb |> #2;
   25.31        val [alpha] = ct |> Thm.ctyp_of_cterm |> Thm.dest_ctyp;
   25.32 -    in (alpha, #1 (dest_Var (Thm.term_of ct))) end;
   25.33 +    in (dest_TVar (Thm.typ_of alpha), #1 (dest_Var (Thm.term_of ct))) end;
   25.34  in
   25.35  
   25.36  fun subtractProver ctxt (Const (@{const_name Tip}, T)) ct dist_thm =
   25.37 @@ -296,7 +300,7 @@
   25.38        in
   25.39          Thm.instantiate
   25.40            ([(alpha, Thm.ctyp_of ctxt alphaI)],
   25.41 -           [(Thm.cterm_of ctxt (Var (v, treeT alphaI)), ct')]) @{thm subtract_Tip}
   25.42 +           [((v, treeT alphaI), ct')]) @{thm subtract_Tip}
   25.43        end
   25.44    | subtractProver ctxt (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm =
   25.45        let
    26.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Fri Jul 03 16:19:45 2015 +0200
    26.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Sun Jul 05 15:02:30 2015 +0200
    26.3 @@ -570,14 +570,14 @@
    26.4        diff (Proof_Context.theory_of ctxt) (scheme_t, instance_t)
    26.5  
    26.6      (*valuation of type variables*)
    26.7 -    val typeval = map (apply2 (Thm.ctyp_of ctxt)) type_pairing
    26.8 +    val typeval = map (fn (v, T) => (dest_TVar v, Thm.ctyp_of ctxt T)) type_pairing
    26.9  
   26.10      val typeval_env =
   26.11        map (apfst dest_TVar) type_pairing
   26.12      (*valuation of term variables*)
   26.13      val termval =
   26.14 -      map (apfst (type_devar typeval_env)) term_pairing
   26.15 -      |> map (apply2 (Thm.cterm_of ctxt))
   26.16 +      map (apfst (dest_Var o type_devar typeval_env)) term_pairing
   26.17 +      |> map (apsnd (Thm.cterm_of ctxt))
   26.18    in
   26.19      Thm.instantiate (typeval, termval) scheme_thm
   26.20    end
    27.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Jul 03 16:19:45 2015 +0200
    27.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Jul 05 15:02:30 2015 +0200
    27.3 @@ -950,8 +950,8 @@
    27.4      val tactic =
    27.5        if is_none var_opt then no_tac
    27.6        else
    27.7 -        fold (curry (op APPEND)) (map (instantiate_tac (the var_opt)) skolem_cts) no_tac
    27.8 -
    27.9 +        fold (curry (op APPEND))
   27.10 +          (map (instantiate_tac (dest_Var (Thm.term_of (the var_opt)))) skolem_cts) no_tac
   27.11    in
   27.12      tactic st
   27.13    end
    28.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Jul 03 16:19:45 2015 +0200
    28.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Sun Jul 05 15:02:30 2015 +0200
    28.3 @@ -607,9 +607,9 @@
    28.4    let
    28.5      val n = Thm.nprems_of coind;
    28.6      val m = Thm.nprems_of (hd rel_monos) - n;
    28.7 -    fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi)))))
    28.8 -      |> apply2 (Thm.cterm_of ctxt);
    28.9 -    val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
   28.10 +    fun mk_inst phi =
   28.11 +      (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi))))))
   28.12 +    val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst;
   28.13      fun mk_unfold rel_eq rel_mono =
   28.14        let
   28.15          val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
    29.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Jul 03 16:19:45 2015 +0200
    29.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun Jul 05 15:02:30 2015 +0200
    29.3 @@ -685,7 +685,9 @@
    29.4        let
    29.5          val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
    29.6  
    29.7 -        val rho_As = map (apply2 (Thm.ctyp_of lthy)) (map Logic.varifyT_global As ~~ As);
    29.8 +        val rho_As =
    29.9 +          map (fn (T, U) => (dest_TVar T, Thm.ctyp_of lthy U))
   29.10 +            (map Logic.varifyT_global As ~~ As);
   29.11  
   29.12          fun inst_thm t thm =
   29.13            Drule.instantiate' [] [SOME (Thm.cterm_of lthy t)]
    30.1 --- a/src/HOL/Tools/Function/partial_function.ML	Fri Jul 03 16:19:45 2015 +0200
    30.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Sun Jul 05 15:02:30 2015 +0200
    30.3 @@ -200,7 +200,8 @@
    30.4      val (P_var, x_var) =
    30.5         Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop
    30.6        |> strip_comb |> apsnd hd
    30.7 -    val P_rangeT = range_type (snd (Term.dest_Var P_var))
    30.8 +      |> apply2 dest_Var
    30.9 +    val P_rangeT = range_type (snd P_var)
   30.10      val PT = map (snd o dest_Free) args ---> P_rangeT
   30.11      val x_inst = cert (foldl1 HOLogic.mk_prod args)
   30.12      val P_inst = cert (uncurry_n (length args) (Free (P, PT)))
   30.13 @@ -211,7 +212,7 @@
   30.14           THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3
   30.15           THEN CONVERSION (split_params_conv ctxt
   30.16             then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3)
   30.17 -      |> Thm.instantiate ([], [(cert P_var, P_inst), (cert x_var, x_inst)]) 
   30.18 +      |> Thm.instantiate ([], [(P_var, P_inst), (x_var, x_inst)])
   30.19        |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt)
   30.20        |> singleton (Variable.export ctxt' ctxt)
   30.21    in
    31.1 --- a/src/HOL/Tools/Function/relation.ML	Fri Jul 03 16:19:45 2015 +0200
    31.2 +++ b/src/HOL/Tools/Function/relation.ML	Sun Jul 05 15:02:30 2015 +0200
    31.3 @@ -18,8 +18,7 @@
    31.4  fun inst_state_tac ctxt inst =
    31.5    SUBGOAL (fn (goal, _) =>
    31.6      (case Term.add_vars goal [] of
    31.7 -      [v as (_, T)] =>
    31.8 -        PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))]))
    31.9 +      [v as (_, T)] => PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (inst T))]))
   31.10      | _ => no_tac));
   31.11  
   31.12  fun relation_tac ctxt rel i =
   31.13 @@ -39,9 +38,7 @@
   31.14              |> map_types Type_Infer.paramify_vars
   31.15              |> Type.constraint T
   31.16              |> Syntax.check_term ctxt;
   31.17 -        in
   31.18 -          PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt rel')]))
   31.19 -        end
   31.20 +        in PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt rel')])) end
   31.21      | _ => no_tac));
   31.22  
   31.23  fun relation_infer_tac ctxt rel i =
    32.1 --- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Fri Jul 03 16:19:45 2015 +0200
    32.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Sun Jul 05 15:02:30 2015 +0200
    32.3 @@ -23,7 +23,7 @@
    32.4      fun get_lhs thm = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
    32.5      val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
    32.6      val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
    32.7 -    val inst = map2 (curry (apply2 (Thm.cterm_of ctxt))) vars UNIVs
    32.8 +    val inst = map dest_Var vars ~~ map (Thm.cterm_of ctxt) UNIVs
    32.9      val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst) 
   32.10        |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
   32.11        |> (fn thm => thm RS sym)
    33.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Fri Jul 03 16:19:45 2015 +0200
    33.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Sun Jul 05 15:02:30 2015 +0200
    33.3 @@ -310,7 +310,7 @@
    33.4      val thy = Proof_Context.theory_of ctxt
    33.5      val (_, qty_schematic) = quot_thm_rty_qty quot_thm
    33.6      val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty
    33.7 -    fun prep_ty (x, (S, ty)) = apply2 (Thm.ctyp_of ctxt) (TVar (x, S), ty)
    33.8 +    fun prep_ty (x, (S, ty)) = ((x, S), Thm.ctyp_of ctxt ty)
    33.9      val ty_inst = Vartab.fold (cons o prep_ty) match_env []
   33.10    in
   33.11      Thm.instantiate (ty_inst, []) quot_thm
    34.1 --- a/src/HOL/Tools/Lifting/lifting_util.ML	Fri Jul 03 16:19:45 2015 +0200
    34.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML	Sun Jul 05 15:02:30 2015 +0200
    34.3 @@ -145,7 +145,7 @@
    34.4  fun instT_thm ctxt env =
    34.5    let
    34.6      val cinst = env |> Vartab.dest 
    34.7 -      |> map (fn (x, (S, T)) => (Thm.ctyp_of ctxt (TVar (x, S)), Thm.ctyp_of ctxt T));
    34.8 +      |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T));
    34.9    in
   34.10      Thm.instantiate (cinst, [])
   34.11    end;
    35.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Jul 03 16:19:45 2015 +0200
    35.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sun Jul 05 15:02:30 2015 +0200
    35.3 @@ -346,16 +346,17 @@
    35.4  (*Replaces universally quantified variables by FREE variables -- because
    35.5    assumptions may not contain scheme variables.  Later, generalize using Variable.export. *)
    35.6  local  
    35.7 -  val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
    35.8 -  val spec_varT = Thm.typ_of_cterm spec_var;
    35.9 -  fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
   35.10 +  val spec_var =
   35.11 +    Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))))
   35.12 +    |> Thm.term_of |> dest_Var;
   35.13 +  fun name_of (Const (@{const_name All}, _) $ Abs(x, _, _)) = x | name_of _ = Name.uu;
   35.14  in  
   35.15    fun freeze_spec th ctxt =
   35.16      let
   35.17        val ([x], ctxt') =
   35.18          Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
   35.19        val spec' = spec
   35.20 -        |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, spec_varT)))]);
   35.21 +        |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]);
   35.22      in (th RS spec', ctxt') end
   35.23  end;
   35.24  
    36.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Jul 03 16:19:45 2015 +0200
    36.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sun Jul 05 15:02:30 2015 +0200
    36.3 @@ -44,10 +44,10 @@
    36.4     "Sledgehammer_Util".) *)
    36.5  fun transform_elim_theorem th =
    36.6    (case Thm.concl_of th of    (*conclusion variable*)
    36.7 -    @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
    36.8 -      Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, cfalse)]) th
    36.9 -  | v as Var(_, @{typ prop}) =>
   36.10 -      Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, ctp_false)]) th
   36.11 +    @{const Trueprop} $ (Var (v as (_, @{typ bool}))) =>
   36.12 +      Thm.instantiate ([], [(v, cfalse)]) th
   36.13 +  | Var (v as (_, @{typ prop})) =>
   36.14 +      Thm.instantiate ([], [(v, ctp_false)]) th
   36.15    | _ => th)
   36.16  
   36.17  
   36.18 @@ -375,9 +375,7 @@
   36.19         th ctxt
   36.20      val (cnf_ths, ctxt) = clausify nnf_th
   36.21      fun intr_imp ct th =
   36.22 -      Thm.instantiate ([], map (apply2 (Thm.cterm_of ctxt))
   36.23 -                               [(Var (("i", 0), @{typ nat}),
   36.24 -                                 HOLogic.mk_nat ax_no)])
   36.25 +      Thm.instantiate ([], [((("i", 0), @{typ nat}), Thm.cterm_of ctxt (HOLogic.mk_nat ax_no))])
   36.26                        (zero_var_indexes @{thm skolem_COMBK_D})
   36.27        RS Thm.implies_intr ct th
   36.28    in
    37.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Jul 03 16:19:45 2015 +0200
    37.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Jul 05 15:02:30 2015 +0200
    37.3 @@ -174,7 +174,7 @@
    37.4  fun incr_type_indexes ctxt inc th =
    37.5    let
    37.6      val tvs = Term.add_tvars (Thm.full_prop_of th) []
    37.7 -    fun inc_tvar ((a, i), s) = apply2 (Thm.ctyp_of ctxt) (TVar ((a, i), s), TVar ((a, i + inc), s))
    37.8 +    fun inc_tvar ((a, i), s) = (((a, i), s), Thm.ctyp_of ctxt (TVar ((a, i + inc), s)))
    37.9    in
   37.10      Thm.instantiate (map inc_tvar tvs, []) th
   37.11    end
   37.12 @@ -211,7 +211,7 @@
   37.13            |> rpair (Envir.empty ~1)
   37.14            |-> fold (Pattern.unify (Context.Proof ctxt))
   37.15            |> Envir.type_env |> Vartab.dest
   37.16 -          |> map (fn (x, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T))
   37.17 +          |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T))
   37.18        in
   37.19          (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
   37.20             "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
   37.21 @@ -400,8 +400,8 @@
   37.22          val thy = Proof_Context.theory_of ctxt
   37.23          val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
   37.24    
   37.25 -        fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (v, S), T)
   37.26 -        fun mk (v, (T, t)) = apply2 (Thm.cterm_of ctxt) (Var (v, Envir.subst_type tyenv T), t)
   37.27 +        fun mkT (v, (S, T)) = ((v, S), Thm.ctyp_of ctxt T)
   37.28 +        fun mk (v, (T, t)) = ((v, Envir.subst_type tyenv T), Thm.cterm_of ctxt t)
   37.29    
   37.30          val instsT = Vartab.fold (cons o mkT) tyenv []
   37.31          val insts = Vartab.fold (cons o mk) tenv []
   37.32 @@ -570,11 +570,11 @@
   37.33              Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
   37.34                tenv = Vartab.empty, tyenv = tyenv}
   37.35            val ty_inst =
   37.36 -            Vartab.fold (fn (x, (S, T)) => cons (apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T)))
   37.37 +            Vartab.fold (fn (x, (S, T)) => cons (((x, S), Thm.ctyp_of ctxt T)))
   37.38                tyenv []
   37.39            val t_inst = [apply2 (Thm.cterm_of ctxt o Envir.norm_term env) (Var var, t')]
   37.40          in
   37.41 -          Drule.instantiate_normalize (ty_inst, t_inst) th
   37.42 +          Drule.instantiate_normalize (ty_inst, map (apfst (dest_Var o Thm.term_of)) t_inst) th
   37.43          end
   37.44        | _ => raise Fail "expected a single non-zapped, non-Metis Var")
   37.45    in
    38.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Jul 03 16:19:45 2015 +0200
    38.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Sun Jul 05 15:02:30 2015 +0200
    38.3 @@ -232,10 +232,10 @@
    38.4  
    38.5      fun instantiate i n ({context = ctxt2, prems, ...}: Subgoal.focus) =
    38.6        let
    38.7 -        fun term_pair_of (ix, (ty, t)) = (Var (ix, ty), t)
    38.8 +        fun inst_pair_of (ix, (ty, t)) = ((ix, ty), t)
    38.9          fun inst_of_matches tts =
   38.10            fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
   38.11 -          |> snd |> Vartab.dest |> map (apply2 (Thm.cterm_of ctxt2) o term_pair_of)
   38.12 +          |> snd |> Vartab.dest |> map (apsnd (Thm.cterm_of ctxt2) o inst_pair_of)
   38.13          val (cases, (eqs, prems1)) = apsnd (chop (nargs - nparams)) (chop n prems)
   38.14          val case_th =
   38.15            rewrite_rule ctxt2 (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
    39.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Jul 03 16:19:45 2015 +0200
    39.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Jul 05 15:02:30 2015 +0200
    39.3 @@ -150,10 +150,10 @@
    39.4  
    39.5  val get_pmi = get_pmi_term o Thm.cprop_of;
    39.6  
    39.7 -val p_v' = @{cpat "?P' :: int => bool"};
    39.8 -val q_v' = @{cpat "?Q' :: int => bool"};
    39.9 -val p_v = @{cpat "?P:: int => bool"};
   39.10 -val q_v = @{cpat "?Q:: int => bool"};
   39.11 +val p_v' = (("P'", 0), @{typ "int \<Rightarrow> bool"});
   39.12 +val q_v' = (("Q'", 0), @{typ "int \<Rightarrow> bool"});
   39.13 +val p_v = (("P", 0), @{typ "int \<Rightarrow> bool"});
   39.14 +val q_v = (("Q", 0), @{typ "int \<Rightarrow> bool"});
   39.15  
   39.16  fun myfwd (th1, th2, th3) p q
   39.17        [(th_1,th_2,th_3), (th_1',th_2',th_3')] =
   39.18 @@ -430,11 +430,13 @@
   39.19  val insert_tm = @{cterm "insert :: int => _"};
   39.20  fun mkISet cts = fold_rev (Thm.apply insert_tm #> Thm.apply) cts emptyIS;
   39.21  val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1;
   39.22 -val [A_tm,B_tm] = map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
   39.23 -                                      |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
   39.24 -                      [asetP,bsetP];
   39.25 +val [A_v,B_v] =
   39.26 +  map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg
   39.27 +    |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
   39.28 +    |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg
   39.29 +    |> Thm.term_of |> dest_Var) [asetP, bsetP];
   39.30  
   39.31 -val D_tm = @{cpat "?D::int"};
   39.32 +val D_v = (("D", 0), @{typ int});
   39.33  
   39.34  fun cooperex_conv ctxt vs q =
   39.35  let
   39.36 @@ -501,16 +503,16 @@
   39.37     if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
   39.38     then
   39.39      (bl,b0,decomp_minf,
   39.40 -     fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
   39.41 +     fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_v,B), (D_v,cd)]) th) dp)
   39.42                       [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
   39.43 -                   (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
   39.44 +                   (map (Thm.instantiate ([],[(B_v,B), (D_v,cd)]))
   39.45                          [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
   39.46                           bsetdisj,infDconj, infDdisj]),
   39.47                         cpmi)
   39.48       else (al,a0,decomp_pinf,fn A =>
   39.49 -          (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
   39.50 +          (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_v,A), (D_v,cd)]) th) dp)
   39.51                     [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
   39.52 -                   (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
   39.53 +                   (map (Thm.instantiate ([],[(A_v,A), (D_v,cd)]))
   39.54                     [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
   39.55                           asetdisj,infDconj, infDdisj]),cppi)
   39.56   val cpth =
    40.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jul 03 16:19:45 2015 +0200
    40.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Jul 05 15:02:30 2015 +0200
    40.3 @@ -73,7 +73,9 @@
    40.4  val lhs = eq |> Thm.dest_arg1;
    40.5  val pt_random_aux = lhs |> Thm.dest_fun;
    40.6  val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun;
    40.7 -val aT = pt_random_aux |> Thm.ctyp_of_cterm |> dest_ctyp_nth 1;
    40.8 +val a_v =
    40.9 +  pt_random_aux |> Thm.ctyp_of_cterm |> dest_ctyp_nth 1
   40.10 +  |> Thm.typ_of |> dest_TVar;
   40.11  
   40.12  val rew_thms = map mk_meta_eq [@{thm natural_zero_minus_one},
   40.13    @{thm Suc_natural_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}];
   40.14 @@ -89,7 +91,7 @@
   40.15        (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
   40.16      val Type (_, [_, iT]) = T;
   40.17      val icT = Thm.ctyp_of lthy iT;
   40.18 -    val inst = Thm.instantiate_cterm ([(aT, icT)], []);
   40.19 +    val inst = Thm.instantiate_cterm ([(a_v, icT)], []);
   40.20      fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
   40.21      val t_rhs = lambda t_k proto_t_rhs;
   40.22      val eqs0 = [subst_v @{term "0::natural"} eq,
   40.23 @@ -98,11 +100,11 @@
   40.24      val ((_, (_, eqs2)), lthy') = lthy
   40.25        |> BNF_LFP_Compat.primrec_simple
   40.26          [((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1;
   40.27 -    val cT_random_aux = inst pt_random_aux;
   40.28 -    val cT_rhs = inst pt_rhs;
   40.29 +    val cT_random_aux = inst pt_random_aux |> Thm.term_of |> dest_Var;
   40.30 +    val cT_rhs = inst pt_rhs |> Thm.term_of |> dest_Var;
   40.31      val rule = @{thm random_aux_rec}
   40.32        |> Drule.instantiate_normalize
   40.33 -        ([(aT, icT)],
   40.34 +        ([(a_v, icT)],
   40.35            [(cT_random_aux, Thm.cterm_of lthy' t_random_aux),
   40.36             (cT_rhs, Thm.cterm_of lthy' t_rhs)]);
   40.37      fun tac ctxt =
    41.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Jul 03 16:19:45 2015 +0200
    41.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Jul 05 15:02:30 2015 +0200
    41.3 @@ -72,20 +72,16 @@
    41.4    | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
    41.5  
    41.6  
    41.7 -fun prep_trm thy (x, (T, t)) =
    41.8 -  (Thm.global_cterm_of thy (Var (x, T)), Thm.global_cterm_of thy t)
    41.9 -
   41.10 -fun prep_ty thy (x, (S, ty)) =
   41.11 -  (Thm.global_ctyp_of thy (TVar (x, S)), Thm.global_ctyp_of thy ty)
   41.12 -
   41.13  fun get_match_inst thy pat trm =
   41.14    let
   41.15      val univ = Unify.matchers (Context.Theory thy) [(pat, trm)]
   41.16      val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *) (* FIXME fragile *)
   41.17      val tenv = Vartab.dest (Envir.term_env env)
   41.18      val tyenv = Vartab.dest (Envir.type_env env)
   41.19 +    fun prep_ty (x, (S, ty)) = ((x, S), Thm.global_ctyp_of thy ty)
   41.20 +    fun prep_trm (x, (T, t)) = ((x, T), Thm.global_cterm_of thy t)
   41.21    in
   41.22 -    (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
   41.23 +    (map prep_ty tyenv, map prep_trm tenv)
   41.24    end
   41.25  
   41.26  (* Calculates the instantiations for the lemmas:
   41.27 @@ -480,7 +476,7 @@
   41.28            then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
   41.29            else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
   41.30          val thm4 =
   41.31 -          Drule.instantiate_normalize ([], [(Thm.cterm_of ctxt insp, Thm.cterm_of ctxt inst)]) thm3
   41.32 +          Drule.instantiate_normalize ([], [(dest_Var insp, Thm.cterm_of ctxt inst)]) thm3
   41.33        in
   41.34          Conv.rewr_conv thm4 ctrm
   41.35        end
    42.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Jul 03 16:19:45 2015 +0200
    42.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sun Jul 05 15:02:30 2015 +0200
    42.3 @@ -35,7 +35,7 @@
    42.4  
    42.5    fun inst f ct thm =
    42.6      let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
    42.7 -    in Thm.instantiate ([], [(cv, ct)]) thm end
    42.8 +    in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end
    42.9  in
   42.10  
   42.11  fun instantiate_elim thm =
   42.12 @@ -199,8 +199,10 @@
   42.13  
   42.14    fun insert_trigger_conv [] ct = Conv.all_conv ct
   42.15      | insert_trigger_conv ctss ct =
   42.16 -        let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
   42.17 -        in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end
   42.18 +        let
   42.19 +          val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
   42.20 +          val inst = map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]
   42.21 +        in Thm.instantiate ([], inst) trigger_eq end
   42.22  
   42.23    fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
   42.24      let
    43.1 --- a/src/HOL/Tools/SMT/smt_util.ML	Fri Jul 03 16:19:45 2015 +0200
    43.2 +++ b/src/HOL/Tools/SMT/smt_util.ML	Sun Jul 05 15:02:30 2015 +0200
    43.3 @@ -171,7 +171,7 @@
    43.4  val destT1 = hd o Thm.dest_ctyp
    43.5  val destT2 = hd o tl o Thm.dest_ctyp
    43.6  
    43.7 -fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
    43.8 +fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct
    43.9  fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
   43.10  fun instT' ct = instT (Thm.ctyp_of_cterm ct)
   43.11  
    44.1 --- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Fri Jul 03 16:19:45 2015 +0200
    44.2 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Jul 05 15:02:30 2015 +0200
    44.3 @@ -100,20 +100,20 @@
    44.4    (Vartab.empty, Vartab.empty)
    44.5    |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t)
    44.6  
    44.7 -fun gen_certify_inst sel mk cert ctxt thm t =
    44.8 +fun gen_certify_inst sel cert ctxt thm t =
    44.9    let
   44.10      val inst = match ctxt (dest_thm thm) (dest_prop t)
   44.11 -    fun cert_inst (ix, (a, b)) = (cert (mk (ix, a)), cert b)
   44.12 +    fun cert_inst (ix, (a, b)) = ((ix, a), cert b)
   44.13    in Vartab.fold (cons o cert_inst) (sel inst) [] end
   44.14  
   44.15  fun match_instantiateT ctxt t thm =
   44.16    if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
   44.17 -    Thm.instantiate (gen_certify_inst fst TVar (Thm.ctyp_of ctxt) ctxt thm t, []) thm
   44.18 +    Thm.instantiate (gen_certify_inst fst (Thm.ctyp_of ctxt) ctxt thm t, []) thm
   44.19    else thm
   44.20  
   44.21  fun match_instantiate ctxt t thm =
   44.22    let val thm' = match_instantiateT ctxt t thm in
   44.23 -    Thm.instantiate ([], gen_certify_inst snd Var (Thm.cterm_of ctxt) ctxt thm' t) thm'
   44.24 +    Thm.instantiate ([], gen_certify_inst snd (Thm.cterm_of ctxt) ctxt thm' t) thm'
   44.25    end
   44.26  
   44.27  fun apply_rule ctxt t =
    45.1 --- a/src/HOL/Tools/SMT/z3_replay_util.ML	Fri Jul 03 16:19:45 2015 +0200
    45.2 +++ b/src/HOL/Tools/SMT/z3_replay_util.ML	Sun Jul 05 15:02:30 2015 +0200
    45.3 @@ -15,7 +15,7 @@
    45.4    val discharge: thm -> thm -> thm
    45.5  
    45.6    (*a faster COMP*)
    45.7 -  type compose_data
    45.8 +  type compose_data = cterm list * (cterm -> cterm list) * thm
    45.9    val precompose: (cterm -> cterm list) -> thm -> compose_data
   45.10    val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
   45.11    val compose: compose_data -> thm -> thm
   45.12 @@ -71,11 +71,12 @@
   45.13  
   45.14  fun list2 (x, y) = [x, y]
   45.15  
   45.16 -fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
   45.17 -fun precompose2 f rule = precompose (list2 o f) rule
   45.18 +fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule)
   45.19 +fun precompose2 f rule : compose_data = precompose (list2 o f) rule
   45.20  
   45.21  fun compose (cvs, f, rule) thm =
   45.22 -  discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
   45.23 +  discharge thm
   45.24 +    (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
   45.25  
   45.26  
   45.27  (* simpset *)
    46.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Fri Jul 03 16:19:45 2015 +0200
    46.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Sun Jul 05 15:02:30 2015 +0200
    46.3 @@ -592,11 +592,10 @@
    46.4      fun prep a = the (AList.lookup (op =) tab a)
    46.5      val thm = transfer_rule_of_terms fst ctxt' tab s t
    46.6      val binsts = bool_insts (if equiv then 0 else 1) (s, t)
    46.7 -    val cbool = @{ctyp bool}
    46.8 -    val relT = @{typ "bool => bool => bool"}
    46.9      val idx = Thm.maxidx_of thm + 1
   46.10 -    fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool)
   46.11 -    fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t)
   46.12 +    fun tinst (a, _) = (((a, idx), @{sort type}), @{ctyp bool})
   46.13 +    fun inst (a, t) =
   46.14 +      ((Name.clean_index (prep a, idx), @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"}), Thm.cterm_of ctxt' t)
   46.15    in
   46.16      thm
   46.17        |> Thm.generalize (tfrees, rnames @ frees) idx
   46.18 @@ -616,11 +615,10 @@
   46.19      fun prep a = the (AList.lookup (op =) tab a)
   46.20      val thm = transfer_rule_of_terms snd ctxt' tab t s
   46.21      val binsts = bool_insts 1 (s, t)
   46.22 -    val cbool = @{ctyp bool}
   46.23 -    val relT = @{typ "bool => bool => bool"}
   46.24      val idx = Thm.maxidx_of thm + 1
   46.25 -    fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool)
   46.26 -    fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t)
   46.27 +    fun tinst (a, _) = (((a, idx), @{sort type}), @{ctyp bool})
   46.28 +    fun inst (a, t) =
   46.29 +      ((Name.clean_index (prep a, idx), @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"}), Thm.cterm_of ctxt' t)
   46.30    in
   46.31      thm
   46.32        |> Thm.generalize (tfrees, rnames @ frees) idx
    47.1 --- a/src/HOL/Tools/coinduction.ML	Fri Jul 03 16:19:45 2015 +0200
    47.2 +++ b/src/HOL/Tools/coinduction.ML	Sun Jul 05 15:02:30 2015 +0200
    47.3 @@ -61,9 +61,9 @@
    47.4              |> fold Variable.declare_names vars
    47.5              |> fold Variable.declare_thm (raw_thm :: prems);
    47.6            val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
    47.7 -          val (rhoTs, rhots) = Thm.match (thm_concl, concl)
    47.8 -            |>> map (apply2 Thm.typ_of)
    47.9 -            ||> map (apply2 Thm.term_of);
   47.10 +          val (instT, inst) = Thm.match (thm_concl, concl);
   47.11 +          val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
   47.12 +          val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
   47.13            val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
   47.14              |> map (subst_atomic_types rhoTs);
   47.15            val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
   47.16 @@ -160,4 +160,3 @@
   47.17  end;
   47.18  
   47.19  end;
   47.20 -
    48.1 --- a/src/HOL/Tools/hologic.ML	Fri Jul 03 16:19:45 2015 +0200
    48.2 +++ b/src/HOL/Tools/hologic.ML	Sun Jul 05 15:02:30 2015 +0200
    48.3 @@ -207,14 +207,14 @@
    48.4    let
    48.5      val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
    48.6        handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
    48.7 -    val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
    48.8 +    val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
    48.9    in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
   48.10  
   48.11  fun conj_elim ctxt thPQ =
   48.12    let
   48.13      val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
   48.14        handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
   48.15 -    val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
   48.16 +    val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
   48.17      val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
   48.18      val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ;
   48.19    in (thP, thQ) end;
    49.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Jul 03 16:19:45 2015 +0200
    49.2 +++ b/src/HOL/Tools/inductive_set.ML	Sun Jul 05 15:02:30 2015 +0200
    49.3 @@ -205,7 +205,7 @@
    49.4        val x' = map_type
    49.5          (K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
    49.6      in
    49.7 -      (Thm.cterm_of ctxt x,
    49.8 +      (dest_Var x,
    49.9         Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
   49.10           (HOLogic.Collect_const U $
   49.11              HOLogic.mk_psplits ps U HOLogic.boolT
   49.12 @@ -367,7 +367,7 @@
   49.13          val T = HOLogic.mk_ptupleT ps Us;
   49.14          val x' = map_type (K (Rs ---> HOLogic.mk_setT T)) x
   49.15        in
   49.16 -        (Thm.cterm_of ctxt x,
   49.17 +        (dest_Var x,
   49.18           Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
   49.19            (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (k downto 0)),
   49.20               list_comb (x', map Bound (l - 1 downto k + 1))))))
    50.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Jul 03 16:19:45 2015 +0200
    50.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Jul 05 15:02:30 2015 +0200
    50.3 @@ -60,10 +60,8 @@
    50.4  fun is_nat t = (fastype_of1 t = HOLogic.natT);
    50.5  
    50.6  fun mk_nat_thm thy t =
    50.7 -  let
    50.8 -    val cn = Thm.global_cterm_of thy (Var (("n", 0), HOLogic.natT))
    50.9 -    and ct = Thm.global_cterm_of thy t
   50.10 -  in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end;
   50.11 +  let val ct = Thm.global_cterm_of thy t
   50.12 +  in Drule.instantiate_normalize ([], [((("n", 0), HOLogic.natT), ct)]) @{thm le0} end;
   50.13  
   50.14  end;
   50.15  
    51.1 --- a/src/HOL/Tools/monomorph.ML	Fri Jul 03 16:19:45 2015 +0200
    51.2 +++ b/src/HOL/Tools/monomorph.ML	Sun Jul 05 15:02:30 2015 +0200
    51.3 @@ -159,7 +159,7 @@
    51.4  
    51.5  fun instantiate ctxt subst =
    51.6    let
    51.7 -    fun cert (ix, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (ix, S), T)
    51.8 +    fun cert (ix, (S, T)) = ((ix, S), Thm.ctyp_of ctxt T)
    51.9      fun cert' subst = Vartab.fold (cons o cert) subst []
   51.10    in Thm.instantiate (cert' subst, []) end
   51.11  
    52.1 --- a/src/HOL/Tools/numeral.ML	Fri Jul 03 16:19:45 2015 +0200
    52.2 +++ b/src/HOL/Tools/numeral.ML	Sun Jul 05 15:02:30 2015 +0200
    52.3 @@ -49,7 +49,7 @@
    52.4  val uminus = @{cpat "uminus"};
    52.5  val uminusT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm uminus));
    52.6  
    52.7 -fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
    52.8 +fun instT T V = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of V), T)], []);
    52.9  
   52.10  in
   52.11  
    53.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Fri Jul 03 16:19:45 2015 +0200
    53.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sun Jul 05 15:02:30 2015 +0200
    53.3 @@ -595,8 +595,8 @@
    53.4  
    53.5   fun prove_nz ctxt T t =
    53.6      let
    53.7 -      val z = Thm.instantiate_cterm ([(zT,T)],[]) zr
    53.8 -      val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq
    53.9 +      val z = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of zT), T)],[]) zr
   53.10 +      val eq = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of eqT), T)],[]) geq
   53.11        val th = Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
   53.12             (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"}
   53.13                    (Thm.apply (Thm.apply eq t) z)))
    54.1 --- a/src/HOL/Tools/record.ML	Fri Jul 03 16:19:45 2015 +0200
    54.2 +++ b/src/HOL/Tools/record.ML	Sun Jul 05 15:02:30 2015 +0200
    54.3 @@ -1755,7 +1755,7 @@
    54.4        fun mk_eq_refl thy =
    54.5          @{thm equal_refl}
    54.6          |> Thm.instantiate
    54.7 -          ([apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
    54.8 +          ([((("'a", 0), @{sort equal}), Thm.global_ctyp_of thy (Logic.varifyT_global extT))], [])
    54.9          |> Axclass.unoverload thy;
   54.10        val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
   54.11        val ensure_exhaustive_record =
    55.1 --- a/src/HOL/Tools/reification.ML	Fri Jul 03 16:19:45 2015 +0200
    55.2 +++ b/src/HOL/Tools/reification.ML	Sun Jul 05 15:02:30 2015 +0200
    55.3 @@ -169,9 +169,9 @@
    55.4            val (fnvs, invs) = List.partition (fn ((vn, _),_) => member (op =) vns vn) (Vartab.dest tmenv);
    55.5            val (fts, its) =
    55.6              (map (snd o snd) fnvs,
    55.7 -             map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of ctxt) (Var ((vn, vi), tT), t)) invs);
    55.8 +             map (fn ((vn, vi), (tT, t)) => (((vn, vi), tT), Thm.cterm_of ctxt t)) invs);
    55.9            val ctyenv =
   55.10 -            map (fn ((vn, vi), (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar ((vn, vi), s), ty))
   55.11 +            map (fn ((vn, vi), (s, ty)) => (((vn, vi), s), Thm.ctyp_of ctxt ty))
   55.12                (Vartab.dest tyenv);
   55.13          in
   55.14            ((map (Thm.cterm_of ctxt) fts ~~ replicate (length fts) ctxt,
   55.15 @@ -203,7 +203,7 @@
   55.16          val sbst = Envir.subst_term (tyenv, tmenv);
   55.17          val sbsT = Envir.subst_type tyenv;
   55.18          val subst_ty =
   55.19 -          map (fn (n, (s, t)) => apply2 (Thm.ctyp_of ctxt'') (TVar (n, s), t)) (Vartab.dest tyenv)
   55.20 +          map (fn (n, (s, t)) => ((n, s), Thm.ctyp_of ctxt'' t)) (Vartab.dest tyenv)
   55.21          val tml = Vartab.dest tmenv;
   55.22          val (subst_ns, bds) = fold_map
   55.23            (fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds =>
   55.24 @@ -230,7 +230,9 @@
   55.25            let
   55.26              val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, []));
   55.27            in map (apply2 ih) (subst_ns @ subst_vs @ cts) end;
   55.28 -        val th = (Drule.instantiate_normalize (subst_ty, substt) eq) RS sym;
   55.29 +        val th =
   55.30 +          (Drule.instantiate_normalize (subst_ty, map (apfst (dest_Var o Thm.term_of)) substt) eq)
   55.31 +            RS sym;
   55.32        in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
   55.33        handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds);
   55.34  
   55.35 @@ -266,10 +268,7 @@
   55.36        let
   55.37          val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop
   55.38            |> HOLogic.dest_eq |> fst |> strip_comb;
   55.39 -        val subst =
   55.40 -          map_filter
   55.41 -            (fn (v as Var (_, T)) => SOME (Thm.cterm_of ctxt' v, subst T)
   55.42 -              | _ => NONE) vs;
   55.43 +        val subst = map_filter (fn Var v => SOME (v, subst (#2 v)) | _ => NONE) vs;
   55.44        in Thm.instantiate ([], subst) eq end;
   55.45      val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs;
   55.46      val bds = AList.make (K ([], [])) tys;
   55.47 @@ -285,9 +284,10 @@
   55.48        | is_list_var _ = false;
   55.49      val vars = th |> Thm.prop_of |> Logic.dest_equals |> snd
   55.50        |> strip_comb |> snd |> filter is_list_var;
   55.51 -    val vs = map (fn v as Var (_, T) =>
   55.52 +    val vs = map (fn Var (v as (_, T)) =>
   55.53        (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars;
   55.54 -    val th' = Drule.instantiate_normalize ([], map (apply2 (Thm.cterm_of ctxt)) vs) th;
   55.55 +    val th' =
   55.56 +      Drule.instantiate_normalize ([], map (apsnd (Thm.cterm_of ctxt)) vs) th;
   55.57      val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th'));
   55.58    in Thm.transitive th'' th' end;
   55.59  
    56.1 --- a/src/HOL/Tools/sat.ML	Fri Jul 03 16:19:45 2015 +0200
    56.2 +++ b/src/HOL/Tools/sat.ML	Sun Jul 05 15:02:30 2015 +0200
    56.3 @@ -73,8 +73,6 @@
    56.4  val resolution_thm =
    56.5    @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
    56.6  
    56.7 -val cP = Thm.cterm_of @{context} (Var (("P", 0), HOLogic.boolT));
    56.8 -
    56.9  (* ------------------------------------------------------------------------- *)
   56.10  (* lit_ord: an order on integers that considers their absolute values only,  *)
   56.11  (*      thereby treating integers that represent the same atom (positively   *)
   56.12 @@ -173,7 +171,7 @@
   56.13                  val cLit =
   56.14                    snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1))  (* strip Trueprop *)
   56.15                in
   56.16 -                Thm.instantiate ([], [(cP, cLit)]) resolution_thm
   56.17 +                Thm.instantiate ([], [((("P", 0), HOLogic.boolT), cLit)]) resolution_thm
   56.18                end
   56.19  
   56.20              val _ =
    57.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Fri Jul 03 16:19:45 2015 +0200
    57.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Sun Jul 05 15:02:30 2015 +0200
    57.3 @@ -238,7 +238,7 @@
    57.4    if is_binop ct ct' then Thm.dest_binop ct'
    57.5    else raise CTERM ("dest_binop: bad binop", [ct, ct'])
    57.6  
    57.7 -fun inst_thm inst = Thm.instantiate ([], inst);
    57.8 +fun inst_thm inst = Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) inst);
    57.9  
   57.10  val dest_number = Thm.term_of #> HOLogic.dest_number #> snd;
   57.11  val is_number = can dest_number;
   57.12 @@ -300,7 +300,7 @@
   57.13          val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
   57.14          val neg_tm = Thm.dest_fun neg_pat
   57.15          val dest_sub = dest_binop sub_tm
   57.16 -      in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub, neg_mul |> concl |> Thm.dest_arg,
   57.17 +      in (neg_mul, sub_add, sub_tm, neg_tm, dest_sub, neg_mul |> concl |> Thm.dest_arg,
   57.18            sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
   57.19        end
   57.20      | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), true_tm, true_tm));
   57.21 @@ -760,7 +760,7 @@
   57.22  fun polynomial_neg_conv ctxt tm =
   57.23     let val (l,r) = Thm.dest_comb tm in
   57.24          if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
   57.25 -        let val th1 = inst_thm [(cx',r)] neg_mul
   57.26 +        let val th1 = inst_thm [(cx', r)] neg_mul
   57.27              val th2 = Thm.transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
   57.28          in Thm.transitive th2 (polynomial_monomial_mul_conv ctxt (concl th2))
   57.29          end
   57.30 @@ -770,7 +770,7 @@
   57.31  (* Subtraction.                                                              *)
   57.32  fun polynomial_sub_conv ctxt tm =
   57.33    let val (l,r) = dest_sub tm
   57.34 -      val th1 = inst_thm [(cx',l),(cy',r)] sub_add
   57.35 +      val th1 = inst_thm [(cx', l), (cy', r)] sub_add
   57.36        val (tm1,tm2) = Thm.dest_comb(concl th1)
   57.37        val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv ctxt tm2)
   57.38    in Thm.transitive th1 (Thm.transitive th2 (polynomial_add_conv ctxt (concl th2)))
    58.1 --- a/src/HOL/Tools/split_rule.ML	Fri Jul 03 16:19:45 2015 +0200
    58.2 +++ b/src/HOL/Tools/split_rule.ML	Sun Jul 05 15:02:30 2015 +0200
    58.3 @@ -42,7 +42,7 @@
    58.4  fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl =
    58.5        let val T' = HOLogic.flatten_tupleT T1 ---> T2;
    58.6            val newt = ap_split T1 T2 (Var (v, T'));
    58.7 -      in Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (t, newt)]) rl end
    58.8 +      in Thm.instantiate ([], [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end
    58.9    | split_rule_var' _ _ rl = rl;
   58.10  
   58.11  
   58.12 @@ -65,15 +65,15 @@
   58.13                  val ys = Name.variant_list xs (replicate (length Ts) a);
   58.14                in
   58.15                  (xs @ ys,
   58.16 -                  apply2 (Thm.cterm_of ctxt)
   58.17 -                    (v, HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
   58.18 -                      (map (Var o apfst (rpair 0)) (ys ~~ Ts))) :: insts)
   58.19 +                  (dest_Var v,
   58.20 +                    Thm.cterm_of ctxt (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
   58.21 +                      (map (Var o apfst (rpair 0)) (ys ~~ Ts)))) :: insts)
   58.22                end
   58.23            | mk_tuple _ x = x;
   58.24          val newt = ap_split' Us U (Var (v, T'));
   58.25          val (vs', insts) = fold mk_tuple ts (vs, []);
   58.26        in
   58.27 -        (Drule.instantiate_normalize ([], [apply2 (Thm.cterm_of ctxt) (t, newt)] @ insts) rl, vs')
   58.28 +        (Drule.instantiate_normalize ([], ((v, T), Thm.cterm_of ctxt newt) :: insts) rl, vs')
   58.29        end
   58.30    | complete_split_rule_var _ _ x = x;
   58.31  
    59.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jul 03 16:19:45 2015 +0200
    59.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Jul 05 15:02:30 2015 +0200
    59.3 @@ -424,7 +424,7 @@
    59.4              val T = Thm.typ_of_cterm cv
    59.5            in
    59.6              mth
    59.7 -            |> Thm.instantiate ([], [(cv, number_of T n)])
    59.8 +            |> Thm.instantiate ([], [(dest_Var (Thm.term_of cv), number_of T n)])
    59.9              |> rewrite_concl
   59.10              |> discharge_prem
   59.11              handle CTERM _ => mult_by_add n thm
    60.1 --- a/src/Provers/hypsubst.ML	Fri Jul 03 16:19:45 2015 +0200
    60.2 +++ b/src/Provers/hypsubst.ML	Sun Jul 05 15:02:30 2015 +0200
    60.3 @@ -186,10 +186,10 @@
    60.4          val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U));
    60.5        in
    60.6          compose_tac ctxt (true, Drule.instantiate_normalize (instT,
    60.7 -          map (apply2 (Thm.cterm_of ctxt))
    60.8 -            [(Var (ixn, Ts ---> U --> body_type T), u),
    60.9 -             (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
   60.10 -             (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
   60.11 +          map (apsnd (Thm.cterm_of ctxt))
   60.12 +            [((ixn, Ts ---> U --> body_type T), u),
   60.13 +             ((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
   60.14 +             ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
   60.15            Thm.nprems_of rl) i
   60.16        end
   60.17    | NONE => no_tac);
    61.1 --- a/src/Pure/Isar/element.ML	Fri Jul 03 16:19:45 2015 +0200
    61.2 +++ b/src/Pure/Isar/element.ML	Sun Jul 05 15:02:30 2015 +0200
    61.3 @@ -201,7 +201,7 @@
    61.4      SOME C =>
    61.5        let
    61.6          val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
    61.7 -        val th' = Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (C, thesis)]) th;
    61.8 +        val th' = Thm.instantiate ([], [(Term.dest_Var C, Thm.cterm_of ctxt thesis)]) th;
    61.9        in (th', true) end
   61.10    | NONE => (th, false));
   61.11  
   61.12 @@ -340,7 +340,7 @@
   61.13  fun instantiate_tfrees thy subst th =
   61.14    let
   61.15      val idx = Thm.maxidx_of th + 1;
   61.16 -    fun cert_inst (a, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar ((a, idx), S), T);
   61.17 +    fun cert_inst (a, (S, T)) = (((a, idx), S), Thm.global_ctyp_of thy T);
   61.18  
   61.19      fun add_inst (a, S) insts =
   61.20        if AList.defined (op =) insts a then insts
    62.1 --- a/src/Pure/Isar/generic_target.ML	Fri Jul 03 16:19:45 2015 +0200
    62.2 +++ b/src/Pure/Isar/generic_target.ML	Sun Jul 05 15:02:30 2015 +0200
    62.3 @@ -271,12 +271,13 @@
    62.4        |>> map Logic.dest_type;
    62.5  
    62.6      val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
    62.7 -    val inst = filter (is_Var o fst) (vars ~~ frees);
    62.8 -    val cinstT = instT
    62.9 -      |> map (apply2 (Thm.ctyp_of ctxt) o apfst TVar);
   62.10 -    val cinst = inst
   62.11 -      |> map (apply2 (Thm.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT)));
   62.12 -    val result' = Thm.instantiate (cinstT, cinst) result;
   62.13 +    val inst =
   62.14 +      map_filter
   62.15 +        (fn (Var (xi, T), t) =>
   62.16 +          SOME ((xi, Term_Subst.instantiateT instT T),
   62.17 +            Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t))
   62.18 +        | _ => NONE) (vars ~~ frees);
   62.19 +    val result' = Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt)) instT, inst) result;
   62.20  
   62.21      (*import assumes/defines*)
   62.22      val result'' =
    63.1 --- a/src/Pure/Isar/obtain.ML	Fri Jul 03 16:19:45 2015 +0200
    63.2 +++ b/src/Pure/Isar/obtain.ML	Sun Jul 05 15:02:30 2015 +0200
    63.3 @@ -334,7 +334,7 @@
    63.4  
    63.5      val instT =
    63.6        fold (Term.add_tvarsT o #2) params []
    63.7 -      |> map (TVar #> (fn T => apply2 (Thm.ctyp_of ctxt) (T, norm_type T)));
    63.8 +      |> map (fn v => (v, Thm.ctyp_of ctxt (norm_type (TVar v))));
    63.9      val closed_rule = rule
   63.10        |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var))
   63.11        |> Thm.instantiate (instT, []);
    64.1 --- a/src/Pure/Isar/subgoal.ML	Fri Jul 03 16:19:45 2015 +0200
    64.2 +++ b/src/Pure/Isar/subgoal.ML	Sun Jul 05 15:02:30 2015 +0200
    64.3 @@ -12,8 +12,9 @@
    64.4  
    64.5  signature SUBGOAL =
    64.6  sig
    64.7 -  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
    64.8 -    asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
    64.9 +  type focus =
   64.10 +   {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
   64.11 +    concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}
   64.12    val focus_params: Proof.context -> int -> thm -> focus * thm
   64.13    val focus_params_fixed: Proof.context -> int -> thm -> focus * thm
   64.14    val focus_prems: Proof.context -> int -> thm -> focus * thm
   64.15 @@ -36,8 +37,9 @@
   64.16  
   64.17  (* focus *)
   64.18  
   64.19 -type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
   64.20 -  asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
   64.21 +type focus =
   64.22 + {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
   64.23 +  concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list};
   64.24  
   64.25  fun gen_focus (do_prems, do_concl) ctxt i raw_st =
   64.26    let
   64.27 @@ -100,7 +102,7 @@
   64.28      val (inst1, inst2) =
   64.29        split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
   64.30  
   64.31 -    val th'' = Thm.instantiate ([], inst1) th';
   64.32 +    val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th';
   64.33    in ((inst2, th''), ctxt'') end;
   64.34  
   64.35  (*
    65.1 --- a/src/Pure/Proof/proof_checker.ML	Fri Jul 03 16:19:45 2015 +0200
    65.2 +++ b/src/Pure/Proof/proof_checker.ML	Sun Jul 05 15:02:30 2015 +0200
    65.3 @@ -78,8 +78,8 @@
    65.4            let
    65.5              val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
    65.6              val (fmap, thm') = Thm.varifyT_global' [] thm;
    65.7 -            val ctye = map (apply2 (Thm.global_ctyp_of thy))
    65.8 -              (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
    65.9 +            val ctye =
   65.10 +              (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
   65.11            in
   65.12              Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
   65.13            end;
   65.14 @@ -118,7 +118,7 @@
   65.15                  handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
   65.16                end
   65.17  
   65.18 -          | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
   65.19 +          | thm_of (vs, names) Hs (AbsP (_, SOME t, prf)) =
   65.20                let
   65.21                  val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t));
   65.22                  val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
    66.1 --- a/src/Pure/Tools/rule_insts.ML	Fri Jul 03 16:19:45 2015 +0200
    66.2 +++ b/src/Pure/Tools/rule_insts.ML	Sun Jul 05 15:02:30 2015 +0200
    66.3 @@ -149,8 +149,8 @@
    66.4    in
    66.5      thm
    66.6      |> Drule.instantiate_normalize
    66.7 -      (map (apply2 (Thm.ctyp_of ctxt') o apfst TVar) inst_tvars,
    66.8 -       map (apply2 (Thm.cterm_of ctxt') o apfst Var) inst_vars)
    66.9 +      (map (apsnd (Thm.ctyp_of ctxt')) inst_tvars,
   66.10 +       map (apsnd (Thm.cterm_of ctxt')) inst_vars)
   66.11      |> singleton (Variable.export ctxt' ctxt)
   66.12      |> Rule_Cases.save thm
   66.13    end;
   66.14 @@ -240,13 +240,13 @@
   66.15  
   66.16      val inc = Thm.maxidx_of st + 1;
   66.17      val lift_type = Logic.incr_tvar inc;
   66.18 -    fun lift_var ((a, j), T) = Var ((a, j + inc), paramTs ---> lift_type T);
   66.19 +    fun lift_var ((a, j), T) = ((a, j + inc), paramTs ---> lift_type T);
   66.20      fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t);
   66.21  
   66.22      val inst_tvars' = inst_tvars
   66.23 -      |> map (apply2 (Thm.ctyp_of inst_ctxt o lift_type) o apfst TVar);
   66.24 +      |> map (fn (((a, i), S), T) => (((a, i + inc), S), Thm.ctyp_of inst_ctxt (lift_type T)));
   66.25      val inst_vars' = inst_vars
   66.26 -      |> map (fn (v, t) => apply2 (Thm.cterm_of inst_ctxt) (lift_var v, lift_term t));
   66.27 +      |> map (fn (v, t) => (lift_var v, Thm.cterm_of inst_ctxt (lift_term t)));
   66.28  
   66.29      val thm' = Thm.lift_rule cgoal thm
   66.30        |> Drule.instantiate_normalize (inst_tvars', inst_vars')
   66.31 @@ -262,10 +262,11 @@
   66.32  fun make_elim_preserve ctxt rl =
   66.33    let
   66.34      val maxidx = Thm.maxidx_of rl;
   66.35 +    fun var x = ((x, 0), propT);
   66.36      fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT));
   66.37      val revcut_rl' =
   66.38 -      Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
   66.39 -        (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   66.40 +      Drule.instantiate_normalize ([], [(var "V", cvar ("V", maxidx + 1)),
   66.41 +        (var "W", cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   66.42    in
   66.43      (case Seq.list_of
   66.44        (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
    67.1 --- a/src/Pure/conjunction.ML	Fri Jul 03 16:19:45 2015 +0200
    67.2 +++ b/src/Pure/conjunction.ML	Sun Jul 05 15:02:30 2015 +0200
    67.3 @@ -69,8 +69,8 @@
    67.4  
    67.5  local
    67.6  
    67.7 -val A = read_prop "A" and vA = read_prop "?A";
    67.8 -val B = read_prop "B" and vB = read_prop "?B";
    67.9 +val A = read_prop "A" and vA = (("A", 0), propT);
   67.10 +val B = read_prop "B" and vB = (("B", 0), propT);
   67.11  val C = read_prop "C";
   67.12  val ABC = read_prop "A ==> B ==> C";
   67.13  val A_B = read_prop "A &&& B";
    68.1 --- a/src/Pure/drule.ML	Fri Jul 03 16:19:45 2015 +0200
    68.2 +++ b/src/Pure/drule.ML	Sun Jul 05 15:02:30 2015 +0200
    68.3 @@ -20,7 +20,8 @@
    68.4    val lift_all: Proof.context -> cterm -> thm -> thm
    68.5    val implies_elim_list: thm -> thm list -> thm
    68.6    val implies_intr_list: cterm list -> thm -> thm
    68.7 -  val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    68.8 +  val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
    68.9 +    thm -> thm
   68.10    val zero_var_indexes_list: thm list -> thm list
   68.11    val zero_var_indexes: thm -> thm
   68.12    val implies_intr_hyps: thm -> thm
   68.13 @@ -613,11 +614,9 @@
   68.14  
   68.15  fun mk_term ct =
   68.16    let
   68.17 -    val thy = Thm.theory_of_cterm ct;
   68.18 -    val T = Thm.typ_of_cterm ct;
   68.19 -    val instT = apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), []), T);
   68.20 -    val x = Thm.global_cterm_of thy (Var (("x", 0), T));
   68.21 -  in Thm.instantiate ([instT], [(x, ct)]) termI end;
   68.22 +    val cT = Thm.ctyp_of_cterm ct;
   68.23 +    val T = Thm.typ_of cT;
   68.24 +  in Thm.instantiate ([((("'a", 0), []), cT)], [((("x", 0), T), ct)]) termI end;
   68.25  
   68.26  fun dest_term th =
   68.27    let val cprop = strip_imp_concl (Thm.cprop_of th) in
   68.28 @@ -767,9 +766,9 @@
   68.29          val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0);
   68.30          val instT =
   68.31            Vartab.fold (fn (xi, (S, T)) =>
   68.32 -            cons (apply2 (Thm.global_ctyp_of thy) (TVar (xi, S), Envir.norm_type tye T))) tye [];
   68.33 +            cons ((xi, S), Thm.global_ctyp_of thy (Envir.norm_type tye T))) tye [];
   68.34          val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs;
   68.35 -      in instantiate_normalize (instT, inst) th end
   68.36 +      in instantiate_normalize (instT, map (apfst (Thm.term_of #> dest_Var)) inst) th end
   68.37        handle TERM (msg, _) => raise THM (msg, 0, [th])
   68.38          | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
   68.39  end;
   68.40 @@ -784,27 +783,18 @@
   68.41          map_filter (Option.map Thm.typ_of) cTs,
   68.42          map_filter (Option.map Thm.term_of) cts);
   68.43  
   68.44 -    fun inst_of (v, ct) =
   68.45 -      (Thm.global_cterm_of (Thm.theory_of_cterm ct) (Var v), ct)
   68.46 -        handle TYPE (msg, _, _) => err msg;
   68.47 -
   68.48 -    fun tyinst_of (v, cT) =
   68.49 -      (Thm.global_ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT)
   68.50 -        handle TYPE (msg, _, _) => err msg;
   68.51 -
   68.52      fun zip_vars xs ys =
   68.53        zip_options xs ys handle ListPair.UnequalLengths =>
   68.54          err "more instantiations than variables in thm";
   68.55  
   68.56 -    (*instantiate types first!*)
   68.57      val thm' =
   68.58        if forall is_none cTs then thm
   68.59 -      else Thm.instantiate
   68.60 -        (map tyinst_of (zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
   68.61 +      else
   68.62 +        Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
   68.63      val thm'' =
   68.64        if forall is_none cts then thm'
   68.65 -      else Thm.instantiate
   68.66 -        ([], map inst_of (zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts)) thm';
   68.67 +      else
   68.68 +        Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
   68.69      in thm'' end;
   68.70  
   68.71  
    69.1 --- a/src/Pure/goal.ML	Fri Jul 03 16:19:45 2015 +0200
    69.2 +++ b/src/Pure/goal.ML	Sun Jul 05 15:02:30 2015 +0200
    69.3 @@ -60,9 +60,7 @@
    69.4    -------- (init)
    69.5    C ==> #C
    69.6  *)
    69.7 -val init =
    69.8 -  let val A = #1 (Thm.dest_implies (Thm.cprop_of Drule.protectI))
    69.9 -  in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end;
   69.10 +fun init C = Thm.instantiate ([], [((("A", 0), propT), C)]) Drule.protectI;
   69.11  
   69.12  (*
   69.13    A1 ==> ... ==> An ==> C
   69.14 @@ -134,8 +132,7 @@
   69.15      val fixes = map (Thm.cterm_of ctxt) xs;
   69.16  
   69.17      val tfrees = fold Term.add_tfrees (prop :: As) [];
   69.18 -    val instT =
   69.19 -      map (fn (a, S) => apply2 (Thm.ctyp_of ctxt) (TVar ((a, 0), S), TFree (a, S))) tfrees;
   69.20 +    val instT = map (fn (a, S) => (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))) tfrees;
   69.21  
   69.22      val global_prop =
   69.23        Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))
    70.1 --- a/src/Pure/more_thm.ML	Fri Jul 03 16:19:45 2015 +0200
    70.2 +++ b/src/Pure/more_thm.ML	Sun Jul 05 15:02:30 2015 +0200
    70.3 @@ -62,12 +62,12 @@
    70.4    val forall_elim_vars: int -> thm -> thm
    70.5    val global_certify_inst: theory ->
    70.6      ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
    70.7 -    (ctyp * ctyp) list * (cterm * cterm) list
    70.8 +    ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
    70.9    val global_certify_instantiate: theory ->
   70.10      ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
   70.11    val certify_inst: Proof.context ->
   70.12      ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
   70.13 -    (ctyp * ctyp) list * (cterm * cterm) list
   70.14 +    ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   70.15    val certify_instantiate: Proof.context ->
   70.16      ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
   70.17    val forall_intr_frees: thm -> thm
   70.18 @@ -357,15 +357,15 @@
   70.19  (* certify_instantiate *)
   70.20  
   70.21  fun global_certify_inst thy (instT, inst) =
   70.22 - (map (fn (v, T) => apply2 (Thm.global_ctyp_of thy) (TVar v, T)) instT,
   70.23 -  map (fn (v, t) => apply2 (Thm.global_cterm_of thy) (Var v, t)) inst);
   70.24 + (map (apsnd (Thm.global_ctyp_of thy)) instT,
   70.25 +  map (apsnd (Thm.global_cterm_of thy)) inst);
   70.26  
   70.27  fun global_certify_instantiate thy insts th =
   70.28    Thm.instantiate (global_certify_inst thy insts) th;
   70.29  
   70.30  fun certify_inst ctxt (instT, inst) =
   70.31 - (map (fn (v, T) => apply2 (Thm.ctyp_of ctxt) (TVar v, T)) instT,
   70.32 -  map (fn (v, t) => apply2 (Thm.cterm_of ctxt) (Var v, t)) inst);
   70.33 + (map (apsnd (Thm.ctyp_of ctxt)) instT,
   70.34 +  map (apsnd (Thm.cterm_of ctxt)) inst);
   70.35  
   70.36  fun certify_instantiate ctxt insts th =
   70.37    Thm.instantiate (certify_inst ctxt insts) th;
   70.38 @@ -446,10 +446,12 @@
   70.39  
   70.40  fun stripped_sorts thy t =
   70.41    let
   70.42 -    val tfrees = rev (map TFree (Term.add_tfrees t []));
   70.43 -    val tfrees' = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT (length tfrees));
   70.44 -    val strip = tfrees ~~ tfrees';
   70.45 -    val recover = map (apply2 (Thm.global_ctyp_of thy o Logic.varifyT_global) o swap) strip;
   70.46 +    val tfrees = rev (Term.add_tfrees t []);
   70.47 +    val tfrees' = map (fn a => (a, [])) (Name.invent Name.context Name.aT (length tfrees));
   70.48 +    val recover =
   70.49 +      map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S))))
   70.50 +        tfrees' tfrees;
   70.51 +    val strip = map (apply2 TFree) (tfrees ~~ tfrees');
   70.52      val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
   70.53    in (strip, recover, t') end;
   70.54  
    71.1 --- a/src/Pure/raw_simplifier.ML	Fri Jul 03 16:19:45 2015 +0200
    71.2 +++ b/src/Pure/raw_simplifier.ML	Sun Jul 05 15:02:30 2015 +0200
    71.3 @@ -1044,8 +1044,9 @@
    71.4              then NONE else SOME thm2'))
    71.5    end;
    71.6  
    71.7 -val (cA, (cB, cC)) =
    71.8 -  apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
    71.9 +val vA = (("A", 0), propT);
   71.10 +val vB = (("B", 0), propT);
   71.11 +val vC = (("C", 0), propT);
   71.12  
   71.13  fun transitive1 NONE NONE = NONE
   71.14    | transitive1 (SOME thm1) NONE = SOME thm1
   71.15 @@ -1177,7 +1178,7 @@
   71.16          val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
   71.17          val eq' =
   71.18            Thm.implies_elim
   71.19 -            (Thm.instantiate ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
   71.20 +            (Thm.instantiate ([], [(vA, prem), (vB, lhs), (vC, rhs)]) Drule.imp_cong)
   71.21              (Thm.implies_intr prem eq);
   71.22        in
   71.23          if not r then eq'
   71.24 @@ -1188,9 +1189,9 @@
   71.25            in
   71.26              Thm.transitive
   71.27                (Thm.transitive
   71.28 -                (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) Drule.swap_prems_eq)
   71.29 +                (Thm.instantiate ([], [(vA, prem'), (vB, prem), (vC, concl)]) Drule.swap_prems_eq)
   71.30                  eq')
   71.31 -              (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) Drule.swap_prems_eq)
   71.32 +              (Thm.instantiate ([], [(vA, prem), (vB, prem''), (vC, concl)]) Drule.swap_prems_eq)
   71.33            end
   71.34        end
   71.35  
    72.1 --- a/src/Pure/thm.ML	Fri Jul 03 16:19:45 2015 +0200
    72.2 +++ b/src/Pure/thm.ML	Sun Jul 05 15:02:30 2015 +0200
    72.3 @@ -47,8 +47,10 @@
    72.4    val lambda: cterm -> cterm -> cterm
    72.5    val adjust_maxidx_cterm: int -> cterm -> cterm
    72.6    val incr_indexes_cterm: int -> cterm -> cterm
    72.7 -  val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
    72.8 -  val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
    72.9 +  val match: cterm * cterm ->
   72.10 +    ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   72.11 +  val first_order_match: cterm * cterm ->
   72.12 +    ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   72.13    (*theorems*)
   72.14    val rep_thm: thm ->
   72.15     {thy: theory,
   72.16 @@ -120,8 +122,10 @@
   72.17    val equal_elim: thm -> thm -> thm
   72.18    val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
   72.19    val generalize: string list * string list -> int -> thm -> thm
   72.20 -  val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   72.21 -  val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
   72.22 +  val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
   72.23 +    thm -> thm
   72.24 +  val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
   72.25 +    cterm -> cterm
   72.26    val trivial: cterm -> thm
   72.27    val of_class: ctyp * class -> thm
   72.28    val strip_shyps: thm -> thm
   72.29 @@ -312,12 +316,10 @@
   72.30      val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty);
   72.31      val sorts = Sorts.union sorts1 sorts2;
   72.32      fun mk_cTinst ((a, i), (S, T)) =
   72.33 -      (Ctyp {T = TVar ((a, i), S), thy = thy, maxidx = i, sorts = sorts},
   72.34 -       Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts});
   72.35 -    fun mk_ctinst ((x, i), (T, t)) =
   72.36 -      let val T = Envir.subst_type Tinsts T in
   72.37 -        (Cterm {t = Var ((x, i), T), T = T, thy = thy, maxidx = i, sorts = sorts},
   72.38 -         Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts})
   72.39 +      (((a, i), S), Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts});
   72.40 +    fun mk_ctinst ((x, i), (U, t)) =
   72.41 +      let val T = Envir.subst_type Tinsts U in
   72.42 +        (((x, i), T), Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts})
   72.43        end;
   72.44    in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end;
   72.45  
   72.46 @@ -1091,37 +1093,28 @@
   72.47  fun pretty_typing thy t T = Pretty.block
   72.48    [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T];
   72.49  
   72.50 -fun add_inst (ct, cu) (thy, sorts) =
   72.51 +fun add_inst (v as (_, T), cu) (thy, sorts) =
   72.52    let
   72.53 -    val Cterm {t = t, T = T, ...} = ct;
   72.54 -    val Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
   72.55 -    val thy' = Theory.merge (thy, merge_thys0 ct cu);
   72.56 +    val Cterm {t = u, T = U, thy = thy2, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
   72.57 +    val thy' = Theory.merge (thy, thy2);
   72.58      val sorts' = Sorts.union sorts_u sorts;
   72.59    in
   72.60 -    (case t of Var v =>
   72.61 -      if T = U then ((v, (u, maxidx_u)), (thy', sorts'))
   72.62 -      else raise TYPE (Pretty.string_of (Pretty.block
   72.63 +    if T = U then ((v, (u, maxidx_u)), (thy', sorts'))
   72.64 +    else
   72.65 +      raise TYPE (Pretty.string_of (Pretty.block
   72.66         [Pretty.str "instantiate: type conflict",
   72.67 -        Pretty.fbrk, pretty_typing thy' t T,
   72.68 -        Pretty.fbrk, pretty_typing thy' u U]), [T, U], [t, u])
   72.69 -    | _ => raise TYPE (Pretty.string_of (Pretty.block
   72.70 -       [Pretty.str "instantiate: not a variable",
   72.71 -        Pretty.fbrk, Syntax.pretty_term_global thy' t]), [], [t]))
   72.72 +        Pretty.fbrk, pretty_typing thy' (Var v) T,
   72.73 +        Pretty.fbrk, pretty_typing thy' u U]), [T, U], [Var v, u])
   72.74    end;
   72.75  
   72.76 -fun add_instT (cT, cU) (thy, sorts) =
   72.77 +fun add_instT (v as (_, S), cU) (thy, sorts) =
   72.78    let
   72.79 -    val Ctyp {T, thy = thy1, ...} = cT
   72.80 -    and Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU;
   72.81 -    val thy' = Theory.merge (thy, Theory.merge (thy1, thy2));
   72.82 +    val Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU;
   72.83 +    val thy' = Theory.merge (thy, thy2);
   72.84      val sorts' = Sorts.union sorts_U sorts;
   72.85    in
   72.86 -    (case T of TVar (v as (_, S)) =>
   72.87 -      if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts'))
   72.88 -      else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], [])
   72.89 -    | _ => raise TYPE (Pretty.string_of (Pretty.block
   72.90 -        [Pretty.str "instantiate: not a type variable",
   72.91 -         Pretty.fbrk, Syntax.pretty_typ_global thy' T]), [T], []))
   72.92 +    if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts'))
   72.93 +    else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], [])
   72.94    end;
   72.95  
   72.96  in
    73.1 --- a/src/Pure/variable.ML	Fri Jul 03 16:19:45 2015 +0200
    73.2 +++ b/src/Pure/variable.ML	Sun Jul 05 15:02:30 2015 +0200
    73.3 @@ -71,10 +71,11 @@
    73.4      (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
    73.5    val importT_terms: term list -> Proof.context -> term list * Proof.context
    73.6    val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
    73.7 -  val importT: thm list -> Proof.context -> ((ctyp * ctyp) list * thm list) * Proof.context
    73.8 +  val importT: thm list -> Proof.context ->
    73.9 +    (((indexname * sort) * ctyp) list * thm list) * Proof.context
   73.10    val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
   73.11    val import: bool -> thm list -> Proof.context ->
   73.12 -    (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context
   73.13 +    ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context
   73.14    val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   73.15    val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   73.16    val focus_params: term -> Proof.context -> (string list * (string * typ) list) * Proof.context
    74.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Fri Jul 03 16:19:45 2015 +0200
    74.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Sun Jul 05 15:02:30 2015 +0200
    74.3 @@ -174,7 +174,7 @@
    74.4      val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
    74.5  
    74.6      (* certified instantiations for types *)
    74.7 -    val ctyp_insts = map (fn (ix, (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (ix, s), ty)) typinsts;
    74.8 +    val ctyp_insts = map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts;
    74.9  
   74.10      (* type instantiated versions *)
   74.11      val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
   74.12 @@ -198,7 +198,7 @@
   74.13  
   74.14      (* create certms of instantiations *)
   74.15      val cinsts_tyinst =
   74.16 -      map (fn (ix, (ty, t)) => apply2 (Thm.cterm_of ctxt) (Var (ix, ty), t)) insts_tyinst_inst;
   74.17 +      map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst;
   74.18  
   74.19      (* The instantiated rule *)
   74.20      val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
   74.21 @@ -217,7 +217,7 @@
   74.22      val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst);
   74.23      val (cprems, abstract_rule_inst) =
   74.24        rule_inst
   74.25 -      |> Thm.instantiate ([], cterm_renamings)
   74.26 +      |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings)
   74.27        |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
   74.28      val specific_tgt_rule =
   74.29        Conv.fconv_rule Drule.beta_eta_conversion
   74.30 @@ -227,7 +227,7 @@
   74.31      val tgt_th_inst =
   74.32        tgt_th_tyinst
   74.33        |> Thm.instantiate ([], cinsts_tyinst)
   74.34 -      |> Thm.instantiate ([], cterm_renamings);
   74.35 +      |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings);
   74.36  
   74.37      val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
   74.38    in
    75.1 --- a/src/Tools/coherent.ML	Fri Jul 03 16:19:45 2015 +0200
    75.2 +++ b/src/Tools/coherent.ML	Sun Jul 05 15:02:30 2015 +0200
    75.3 @@ -179,10 +179,10 @@
    75.4      val th' =
    75.5        Drule.implies_elim_list
    75.6          (Thm.instantiate
    75.7 -           (map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T)) (Vartab.dest tye),
    75.8 +           (map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye),
    75.9              map (fn (ixn, (T, t)) =>
   75.10 -              apply2 (Thm.cterm_of ctxt) (Var (ixn, Envir.subst_type tye T), t)) (Vartab.dest env) @
   75.11 -            map (fn (ixnT, t) => apply2 (Thm.cterm_of ctxt) (Var ixnT, t)) insts) th)
   75.12 +              ((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @
   75.13 +            map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts) th)
   75.14          (map (nth asms) is);
   75.15      val (_, cases) = dest_elim (Thm.prop_of th');
   75.16    in
    76.1 --- a/src/Tools/induct.ML	Fri Jul 03 16:19:45 2015 +0200
    76.2 +++ b/src/Tools/induct.ML	Sun Jul 05 15:02:30 2015 +0200
    76.3 @@ -573,8 +573,8 @@
    76.4      val pairs = Vartab.dest (Envir.term_env env);
    76.5      val types = Vartab.dest (Envir.type_env env);
    76.6      val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs;
    76.7 -    val xs = map2 (curry (Thm.cterm_of ctxt o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts);
    76.8 -  in (map (fn (xi, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (xi, S), T)) types, xs ~~ ts) end;
    76.9 +    val xs = map #1 pairs ~~ map Thm.typ_of_cterm ts;
   76.10 +  in (map (fn (ai, (S, T)) => ((ai, S), Thm.ctyp_of ctxt T)) types, xs ~~ ts) end;
   76.11  
   76.12  in
   76.13  
    77.1 --- a/src/Tools/misc_legacy.ML	Fri Jul 03 16:19:45 2015 +0200
    77.2 +++ b/src/Tools/misc_legacy.ML	Sun Jul 05 15:02:30 2015 +0200
    77.3 @@ -173,9 +173,9 @@
    77.4            then ((v, T), true, free_of "METAHYP2_" (v, T))
    77.5            else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
    77.6        (*Instantiate subgoal vars by Free applied to params*)
    77.7 -      fun mk_ctpair (v, in_concl, u) =
    77.8 -          if in_concl then apply2 (Thm.cterm_of ctxt) (Var v, u)
    77.9 -          else apply2 (Thm.cterm_of ctxt) (Var v, list_comb (u, fparams))
   77.10 +      fun mk_inst (v, in_concl, u) =
   77.11 +          if in_concl then (v, Thm.cterm_of ctxt u)
   77.12 +          else (v, Thm.cterm_of ctxt (list_comb (u, fparams)))
   77.13        (*Restore Vars with higher type and index*)
   77.14        fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
   77.15            if in_concl then apply2 (Thm.cterm_of ctxt) (u, Var ((a, i), T))
   77.16 @@ -191,7 +191,7 @@
   77.17                fold Term.add_vars (Logic.strip_imp_prems prop) []
   77.18              and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
   77.19              val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   77.20 -            val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
   77.21 +            val st' = Thm.instantiate ([], map mk_inst subgoal_insts) st
   77.22              val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st')
   77.23              val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
   77.24          in  (*restore the unknowns to the hypotheses*)
   77.25 @@ -269,7 +269,7 @@
   77.26               fun thaw i th' = (*i is non-negative increment for Var indexes*)
   77.27                   th' |> forall_intr_list (map #2 insts)
   77.28                       |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
   77.29 -         in  (Thm.instantiate ([],insts) fth, thaw)  end
   77.30 +         in  (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw)  end
   77.31   end;
   77.32  
   77.33  (*Basic version of the function above. No option to rename Vars apart in thaw.
   77.34 @@ -291,7 +291,7 @@
   77.35               fun thaw th' =
   77.36                   th' |> forall_intr_list (map #2 insts)
   77.37                       |> forall_elim_list (map #1 insts)
   77.38 -         in  (Thm.instantiate ([],insts) fth, thaw)  end
   77.39 +         in  (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw)  end
   77.40   end;
   77.41  
   77.42  end;
    78.1 --- a/src/Tools/nbe.ML	Fri Jul 03 16:19:45 2015 +0200
    78.2 +++ b/src/Tools/nbe.ML	Sun Jul 05 15:02:30 2015 +0200
    78.3 @@ -101,11 +101,10 @@
    78.4      val vs_tab = map mk_entry (Term.add_tfrees (Thm.term_of ct) []);
    78.5      fun instantiate thm =
    78.6        let
    78.7 -        val cert_tvars = map (Thm.ctyp_of ctxt o TVar) (Term.add_tvars
    78.8 -          ((fst o Logic.dest_equals o Logic.strip_imp_concl o Thm.prop_of) thm) []);
    78.9 -        val instantiation =
   78.10 -          map2 (fn cert_tvar => fn (_, (_, (cT, _))) => (cert_tvar, cT)) cert_tvars vs_tab;
   78.11 -      in Thm.instantiate (instantiation, []) thm end;
   78.12 +        val tvars =
   78.13 +          Term.add_tvars (#1 (Logic.dest_equals (Logic.strip_imp_concl (Thm.prop_of thm)))) [];
   78.14 +        val instT = map2 (fn v => fn (_, (_, (cT, _))) => (v, cT)) tvars vs_tab;
   78.15 +      in Thm.instantiate (instT, []) thm end;
   78.16      fun of_class (TFree (v, _), class) =
   78.17            the (AList.lookup (op =) ((snd o snd o the o AList.lookup (op =) vs_tab) v) class)
   78.18        | of_class (T, _) = error ("Bad type " ^ Syntax.string_of_typ ctxt T);
    79.1 --- a/src/ZF/Tools/cartprod.ML	Fri Jul 03 16:19:45 2015 +0200
    79.2 +++ b/src/ZF/Tools/cartprod.ML	Sun Jul 05 15:02:30 2015 +0200
    79.3 @@ -109,7 +109,7 @@
    79.4        in
    79.5          remove_split ctxt
    79.6            (Drule.instantiate_normalize ([],
    79.7 -            [apply2 (Thm.cterm_of ctxt) (Var(v, Ind_Syntax.iT-->T2), newt)]) rl)
    79.8 +            [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl)
    79.9        end
   79.10    | split_rule_var _ (t,T,rl) = rl;
   79.11  
    80.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Jul 03 16:19:45 2015 +0200
    80.2 +++ b/src/ZF/Tools/inductive_package.ML	Sun Jul 05 15:02:30 2015 +0200
    80.3 @@ -495,7 +495,7 @@
    80.4         The name "x.1" comes from the "RS spec" !*)
    80.5       val inst =
    80.6           case elem_frees of [_] => I
    80.7 -            | _ => Drule.instantiate_normalize ([], [(Thm.global_cterm_of thy (Var(("x",1), Ind_Syntax.iT)),
    80.8 +            | _ => Drule.instantiate_normalize ([], [(((("x",1), Ind_Syntax.iT)),
    80.9                                        Thm.global_cterm_of thy elem_tuple)]);
   80.10  
   80.11       (*strip quantifier and the implication*)