tuned signature;
authorwenzelm
Mon Jul 27 17:44:55 2015 +0200 (2015-07-27)
changeset 608017664e0916eec
parent 60799 57dd0b45fc21
child 60802 067658d63c5d
tuned signature;
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/commutative_ring_tac.ML
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/cont_proc.ML
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/Import/import_rule.ML
src/HOL/Library/Code_Abstract_Nat.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Probability/measurable.ML
src/HOL/String.thy
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Function/function_context_tree.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Lifting/lifting_term.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/qelim.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/Transfer/transfer_bnf.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/cnf.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/record.ML
src/HOL/Tools/semiring_normalizer.ML
src/Pure/axclass.ML
src/Pure/drule.ML
src/Pure/more_thm.ML
src/Tools/atomize_elim.ML
     1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Jul 27 16:35:12 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Jul 27 17:44:55 2015 +0200
     1.3 @@ -906,7 +906,7 @@
     1.4    let val (a, b) = Rat.quotient_of_rat x
     1.5    in if b = 1 then Numeral.mk_cnumber cT a
     1.6      else Thm.apply
     1.7 -         (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
     1.8 +         (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"})
     1.9                       (Numeral.mk_cnumber cT a))
    1.10           (Numeral.mk_cnumber cT b)
    1.11   end
    1.12 @@ -939,7 +939,7 @@
    1.13                    (if neg then Thm.apply (Thm.apply clt c) cz
    1.14                      else Thm.apply (Thm.apply clt cz) c))
    1.15          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    1.16 -        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
    1.17 +        val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
    1.18               (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
    1.19          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.20                     (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.21 @@ -947,7 +947,7 @@
    1.22      | ("x+t",[t]) =>
    1.23         let
    1.24          val T = Thm.ctyp_of_cterm x
    1.25 -        val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
    1.26 +        val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
    1.27          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.28                (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.29         in  rth end
    1.30 @@ -962,7 +962,7 @@
    1.31                    (if neg then Thm.apply (Thm.apply clt c) cz
    1.32                      else Thm.apply (Thm.apply clt cz) c))
    1.33          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    1.34 -        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
    1.35 +        val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
    1.36               (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
    1.37          val rth = th
    1.38        in rth end
    1.39 @@ -975,7 +975,7 @@
    1.40         let
    1.41          val T = Thm.ctyp_of_cterm x
    1.42          val cr = dest_frac c
    1.43 -        val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
    1.44 +        val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"}
    1.45          val cz = Thm.dest_arg ct
    1.46          val neg = cr </ Rat.zero
    1.47          val cthp = Simplifier.rewrite ctxt
    1.48 @@ -983,7 +983,7 @@
    1.49                    (if neg then Thm.apply (Thm.apply clt c) cz
    1.50                      else Thm.apply (Thm.apply clt cz) c))
    1.51          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    1.52 -        val th = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
    1.53 +        val th = Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [c,x,t])
    1.54               (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
    1.55          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.56                     (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.57 @@ -991,7 +991,7 @@
    1.58      | ("x+t",[t]) =>
    1.59         let
    1.60          val T = Thm.ctyp_of_cterm x
    1.61 -        val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
    1.62 +        val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
    1.63          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.64                (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.65         in  rth end
    1.66 @@ -999,7 +999,7 @@
    1.67         let
    1.68          val T = Thm.ctyp_of_cterm x
    1.69          val cr = dest_frac c
    1.70 -        val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
    1.71 +        val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"}
    1.72          val cz = Thm.dest_arg ct
    1.73          val neg = cr </ Rat.zero
    1.74          val cthp = Simplifier.rewrite ctxt
    1.75 @@ -1007,7 +1007,7 @@
    1.76                    (if neg then Thm.apply (Thm.apply clt c) cz
    1.77                      else Thm.apply (Thm.apply clt cz) c))
    1.78          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    1.79 -        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
    1.80 +        val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
    1.81               (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
    1.82          val rth = th
    1.83        in rth end
    1.84 @@ -1026,14 +1026,14 @@
    1.85               (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
    1.86          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    1.87          val th = Thm.implies_elim
    1.88 -                 (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
    1.89 +                 (Thm.instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
    1.90          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.91                     (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    1.92        in rth end
    1.93      | ("x+t",[t]) =>
    1.94         let
    1.95          val T = Thm.ctyp_of_cterm x
    1.96 -        val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
    1.97 +        val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
    1.98          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    1.99                (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
   1.100         in  rth end
   1.101 @@ -1048,7 +1048,7 @@
   1.102               (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
   1.103          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
   1.104          val rth = Thm.implies_elim
   1.105 -                 (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
   1.106 +                 (Thm.instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
   1.107        in rth end
   1.108      | _ => Thm.reflexive ct);
   1.109  
   1.110 @@ -1062,7 +1062,7 @@
   1.111    Const(@{const_name Orderings.less},_)$a$b =>
   1.112     let val (ca,cb) = Thm.dest_binop ct
   1.113         val T = Thm.ctyp_of_cterm ca
   1.114 -       val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
   1.115 +       val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
   1.116         val nth = Conv.fconv_rule
   1.117           (Conv.arg_conv (Conv.arg1_conv
   1.118                (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
   1.119 @@ -1071,7 +1071,7 @@
   1.120  | Const(@{const_name Orderings.less_eq},_)$a$b =>
   1.121     let val (ca,cb) = Thm.dest_binop ct
   1.122         val T = Thm.ctyp_of_cterm ca
   1.123 -       val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
   1.124 +       val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
   1.125         val nth = Conv.fconv_rule
   1.126           (Conv.arg_conv (Conv.arg1_conv
   1.127                (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
   1.128 @@ -1081,7 +1081,7 @@
   1.129  | Const(@{const_name HOL.eq},_)$a$b =>
   1.130     let val (ca,cb) = Thm.dest_binop ct
   1.131         val T = Thm.ctyp_of_cterm ca
   1.132 -       val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
   1.133 +       val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
   1.134         val nth = Conv.fconv_rule
   1.135           (Conv.arg_conv (Conv.arg1_conv
   1.136                (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
     2.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Mon Jul 27 16:35:12 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Mon Jul 27 17:44:55 2015 +0200
     2.3 @@ -96,7 +96,7 @@
     2.4      val cring_ctxt = ctxt addsimps cring_simps;  (*FIXME really the full simpset!?*)
     2.5      val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g);
     2.6      val norm_eq_th = (* may collapse to True *)
     2.7 -      simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
     2.8 +      simplify cring_ctxt (Thm.instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
     2.9    in
    2.10      cut_tac norm_eq_th i
    2.11      THEN (simp_tac cring_ctxt i)
     3.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Mon Jul 27 16:35:12 2015 +0200
     3.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Mon Jul 27 17:44:55 2015 +0200
     3.3 @@ -87,23 +87,23 @@
     3.4     val q = Thm.rhs_of nth
     3.5     val qx = Thm.rhs_of nthx
     3.6     val enth = Drule.arg_cong_rule ce nthx
     3.7 -   val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
     3.8 +   val [th0,th1] = map (Thm.instantiate' [SOME cT] []) @{thms "finite.intros"}
     3.9     fun ins x th =
    3.10 -      Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
    3.11 +      Thm.implies_elim (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
    3.12                                         (Thm.cprop_of th), SOME x] th1) th
    3.13     val fU = fold ins u th0
    3.14     val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU)
    3.15     local
    3.16 -     val insI1 = instantiate' [SOME cT] [] @{thm "insertI1"}
    3.17 -     val insI2 = instantiate' [SOME cT] [] @{thm "insertI2"}
    3.18 +     val insI1 = Thm.instantiate' [SOME cT] [] @{thm "insertI1"}
    3.19 +     val insI2 = Thm.instantiate' [SOME cT] [] @{thm "insertI2"}
    3.20     in
    3.21      fun provein x S =
    3.22       case Thm.term_of S of
    3.23          Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S])
    3.24        | Const(@{const_name insert}, _) $ y $_ =>
    3.25           let val (cy,S') = Thm.dest_binop S
    3.26 -         in if Thm.term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
    3.27 -         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
    3.28 +         in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1
    3.29 +         else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2)
    3.30                             (provein x S')
    3.31           end
    3.32     end
    3.33 @@ -141,11 +141,11 @@
    3.34                        else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
    3.35                        else raise Fail "decomp_mpinf: Impossible case!!") fm
    3.36               val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
    3.37 -               if c = Nox then map (instantiate' [] [SOME fm])
    3.38 +               if c = Nox then map (Thm.instantiate' [] [SOME fm])
    3.39                                      [minf_P, pinf_P, nmi_P, npi_P, ld_P]
    3.40                 else
    3.41                  let val [mi_th,pi_th,nmi_th,npi_th,ld_th] =
    3.42 -                 map (instantiate' [] [SOME t])
    3.43 +                 map (Thm.instantiate' [] [SOME t])
    3.44                   (case c of Lt => [minf_lt, pinf_lt, nmi_lt, npi_lt, ld_lt]
    3.45                            | Le => [minf_le, pinf_le, nmi_le, npi_le, ld_le]
    3.46                            | Gt => [minf_gt, pinf_gt, nmi_gt, npi_gt, ld_gt]
    3.47 @@ -160,7 +160,7 @@
    3.48     val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q
    3.49     val qe_th = Drule.implies_elim_list
    3.50                    ((fconv_rule (Thm.beta_conversion true))
    3.51 -                   (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
    3.52 +                   (Thm.instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
    3.53                          qe))
    3.54                    [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
    3.55      val bex_conv =
     4.1 --- a/src/HOL/Decision_Procs/langford.ML	Mon Jul 27 16:35:12 2015 +0200
     4.2 +++ b/src/HOL/Decision_Procs/langford.ML	Mon Jul 27 17:44:55 2015 +0200
     4.3 @@ -21,10 +21,10 @@
     4.4  
     4.5  fun prove_finite cT u =
     4.6    let
     4.7 -    val [th0, th1] = map (instantiate' [SOME cT] []) @{thms finite.intros}
     4.8 +    val [th0, th1] = map (Thm.instantiate' [SOME cT] []) @{thms finite.intros}
     4.9      fun ins x th =
    4.10        Thm.implies_elim
    4.11 -        (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
    4.12 +        (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
    4.13    in fold ins u th0 end;
    4.14  
    4.15  fun simp_rule ctxt =
    4.16 @@ -39,7 +39,7 @@
    4.17          val p = Thm.dest_arg ep
    4.18          val ths =
    4.19            simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
    4.20 -            (instantiate' [] [SOME p] stupid)
    4.21 +            (Thm.instantiate' [] [SOME p] stupid)
    4.22          val (L, U) =
    4.23            let val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
    4.24            in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end
    4.25 @@ -47,7 +47,7 @@
    4.26            let
    4.27              val (a, A) = Thm.dest_comb S |>> Thm.dest_arg
    4.28              val cT = Thm.ctyp_of_cterm a
    4.29 -            val ne = instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
    4.30 +            val ne = Thm.instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
    4.31              val f = prove_finite cT (dest_set S)
    4.32           in (ne, f) end
    4.33  
    4.34 @@ -114,7 +114,7 @@
    4.35      val rr = Thm.dest_arg r
    4.36      val thl  = prove_conj tabl (conjuncts rr) |> Drule.implies_intr_hyps
    4.37      val thr  = prove_conj tabr (conjuncts ll) |> Drule.implies_intr_hyps
    4.38 -    val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
    4.39 +    val eqI = Thm.instantiate' [] [SOME ll, SOME rr] @{thm iffI}
    4.40    in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
    4.41  
    4.42  fun contains x ct =
    4.43 @@ -230,7 +230,7 @@
    4.44  
    4.45  fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
    4.46    let
    4.47 -    fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
    4.48 +    fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"}
    4.49      fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
    4.50      val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
    4.51      val p' = fold_rev gen ts p
     5.1 --- a/src/HOL/HOLCF/Cfun.thy	Mon Jul 27 16:35:12 2015 +0200
     5.2 +++ b/src/HOL/HOLCF/Cfun.thy	Mon Jul 27 17:44:55 2015 +0200
     5.3 @@ -145,7 +145,7 @@
     5.4        val dest = Thm.dest_comb;
     5.5        val f = (snd o dest o snd o dest) ct;
     5.6        val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
     5.7 -      val tr = instantiate' [SOME T, SOME U] [SOME f]
     5.8 +      val tr = Thm.instantiate' [SOME T, SOME U] [SOME f]
     5.9            (mk_meta_eq @{thm Abs_cfun_inverse2});
    5.10        val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
    5.11        val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
     6.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Mon Jul 27 16:35:12 2015 +0200
     6.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Mon Jul 27 17:44:55 2015 +0200
     6.3 @@ -213,7 +213,7 @@
     6.4              val (n2, t2) = cons2typ n1 cons
     6.5            in (n2, mk_ssumT (t1, t2)) end
     6.6        val ct = Thm.global_ctyp_of thy (snd (cons2typ 1 spec'))
     6.7 -      val thm1 = instantiate' [SOME ct] [] @{thm exh_start}
     6.8 +      val thm1 = Thm.instantiate' [SOME ct] [] @{thm exh_start}
     6.9        val thm2 = rewrite_rule (Proof_Context.init_global thy)
    6.10          (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
    6.11        val thm3 = rewrite_rule (Proof_Context.init_global thy)
     7.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Jul 27 16:35:12 2015 +0200
     7.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Jul 27 17:44:55 2015 +0200
     7.3 @@ -121,7 +121,7 @@
     7.4  local
     7.5    fun solve_cont ctxt t =
     7.6      let
     7.7 -      val tr = instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
     7.8 +      val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
     7.9      in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end
    7.10  in
    7.11    fun cont_proc thy =
     8.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Mon Jul 27 16:35:12 2015 +0200
     8.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon Jul 27 17:44:55 2015 +0200
     8.3 @@ -153,7 +153,7 @@
     8.4      val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT)
     8.5      val predicate = lambda_tuple lhss (list_comb (P, lhss))
     8.6      val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
     8.7 -      |> Drule.instantiate' [] [SOME (Thm.global_cterm_of thy predicate)]
     8.8 +      |> Thm.instantiate' [] [SOME (Thm.global_cterm_of thy predicate)]
     8.9        |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict}
    8.10      val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
    8.11        |> Local_Defs.unfold lthy @{thms split_conv}
     9.1 --- a/src/HOL/Import/import_rule.ML	Mon Jul 27 16:35:12 2015 +0200
     9.2 +++ b/src/HOL/Import/import_rule.ML	Mon Jul 27 17:44:55 2015 +0200
     9.3 @@ -55,7 +55,7 @@
     9.4    let
     9.5      val (tml, tmr) = Thm.dest_binop (strip_imp_concl (Thm.cprop_of th))
     9.6      val cty = Thm.ctyp_of_cterm tml
     9.7 -    val i = Drule.instantiate' [SOME cty] [SOME tml, SOME tmr]
     9.8 +    val i = Thm.instantiate' [SOME cty] [SOME tml, SOME tmr]
     9.9        @{thm meta_eq_to_obj_eq}
    9.10    in
    9.11      Thm.implies_elim i th
    9.12 @@ -66,7 +66,7 @@
    9.13  fun eq_mp th1 th2 =
    9.14    let
    9.15      val (tm1l, tm1r) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1)))
    9.16 -    val i1 = Drule.instantiate' [] [SOME tm1l, SOME tm1r] @{thm iffD1}
    9.17 +    val i1 = Thm.instantiate' [] [SOME tm1l, SOME tm1r] @{thm iffD1}
    9.18      val i2 = meta_mp i1 th1
    9.19    in
    9.20      meta_mp i2 th2
    9.21 @@ -79,7 +79,7 @@
    9.22      val (cf, cg) = Thm.dest_binop t1c
    9.23      val (cx, cy) = Thm.dest_binop t2c
    9.24      val [fd, fr] = Thm.dest_ctyp (Thm.ctyp_of_cterm cf)
    9.25 -    val i1 = Drule.instantiate' [SOME fd, SOME fr]
    9.26 +    val i1 = Thm.instantiate' [SOME fd, SOME fr]
    9.27        [SOME cf, SOME cg, SOME cx, SOME cy] @{thm cong}
    9.28      val i2 = meta_mp i1 th1
    9.29    in
    9.30 @@ -93,7 +93,7 @@
    9.31      val (r, s) = Thm.dest_binop t1c
    9.32      val (_, t) = Thm.dest_binop t2c
    9.33      val ty = Thm.ctyp_of_cterm r
    9.34 -    val i1 = Drule.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
    9.35 +    val i1 = Thm.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
    9.36      val i2 = meta_mp i1 th1
    9.37    in
    9.38      meta_mp i2 th2
    9.39 @@ -107,7 +107,7 @@
    9.40      val th2a = implies_elim_all th2
    9.41      val th1b = Thm.implies_intr th2c th1a
    9.42      val th2b = Thm.implies_intr th1c th2a
    9.43 -    val i = Drule.instantiate' []
    9.44 +    val i = Thm.instantiate' []
    9.45        [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
    9.46      val i1 = Thm.implies_elim i (Thm.assume (Thm.cprop_of th2b))
    9.47      val i2 = Thm.implies_elim i1 th1b
    9.48 @@ -120,7 +120,7 @@
    9.49  fun conj1 th =
    9.50    let
    9.51      val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
    9.52 -    val i = Drule.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct1}
    9.53 +    val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct1}
    9.54    in
    9.55      meta_mp i th
    9.56    end
    9.57 @@ -128,7 +128,7 @@
    9.58  fun conj2 th =
    9.59    let
    9.60      val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
    9.61 -    val i = Drule.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct2}
    9.62 +    val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct2}
    9.63    in
    9.64      meta_mp i th
    9.65    end
    9.66 @@ -137,7 +137,7 @@
    9.67    let
    9.68      val cty = Thm.ctyp_of_cterm ctm
    9.69    in
    9.70 -    Drule.instantiate' [SOME cty] [SOME ctm] @{thm refl}
    9.71 +    Thm.instantiate' [SOME cty] [SOME ctm] @{thm refl}
    9.72    end
    9.73  
    9.74  fun abs cv th =
    9.75 @@ -151,7 +151,7 @@
    9.76      val th2 = trans (trans bl th1) br
    9.77      val th3 = implies_elim_all th2
    9.78      val th4 = Thm.forall_intr cv th3
    9.79 -    val i = Drule.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)]
    9.80 +    val i = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)]
    9.81        [SOME ll, SOME lr] @{thm ext2}
    9.82    in
    9.83      meta_mp i th4
    9.84 @@ -202,7 +202,7 @@
    9.85      val P = Thm.dest_arg cn
    9.86      val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
    9.87    in
    9.88 -    Drule.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
    9.89 +    Thm.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
    9.90        SOME (Thm.global_cterm_of thy (Free ("a", Thm.typ_of nty))),
    9.91        SOME (Thm.global_cterm_of thy (Free ("r", Thm.typ_of oty)))] @{thm typedef_hol2hollight}
    9.92    end
    9.93 @@ -210,7 +210,7 @@
    9.94  fun tydef' tycname abs_name rep_name cP ct td_th thy =
    9.95    let
    9.96      val ctT = Thm.ctyp_of_cterm ct
    9.97 -    val nonempty = Drule.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
    9.98 +    val nonempty = Thm.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
    9.99      val th2 = meta_mp nonempty td_th
   9.100      val c =
   9.101        case Thm.concl_of th2 of
   9.102 @@ -228,7 +228,7 @@
   9.103      val rept = Thm.dest_arg th_s
   9.104      val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
   9.105      val typedef_th =
   9.106 -       Drule.instantiate'
   9.107 +       Thm.instantiate'
   9.108            [SOME nty, SOME oty]
   9.109            [SOME rept, SOME abst, SOME cP, SOME (Thm.global_cterm_of thy' (Free ("a", aty))),
   9.110               SOME (Thm.global_cterm_of thy' (Free ("r", Thm.typ_of ctT)))]
    10.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Mon Jul 27 16:35:12 2015 +0200
    10.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Mon Jul 27 17:44:55 2015 +0200
    10.3 @@ -77,7 +77,7 @@
    10.4          val thm' =
    10.5            Thm.implies_elim
    10.6             (Conv.fconv_rule (Thm.beta_conversion true)
    10.7 -             (Drule.instantiate'
    10.8 +             (Thm.instantiate'
    10.9                 [SOME (Thm.ctyp_of_cterm ct)] [SOME (Thm.lambda cv ct),
   10.10                   SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv']
   10.11                 Suc_if_eq)) (Thm.forall_intr cv' thm)
    11.1 --- a/src/HOL/Library/Countable.thy	Mon Jul 27 16:35:12 2015 +0200
    11.2 +++ b/src/HOL/Library/Countable.thy	Mon Jul 27 17:44:55 2015 +0200
    11.3 @@ -182,7 +182,7 @@
    11.4          val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
    11.5          val insts = vars |> map (fn (_, T) => try (Thm.cterm_of ctxt)
    11.6            (Const (@{const_name Countable.finite_item}, T)))
    11.7 -        val induct_thm' = Drule.instantiate' [] insts induct_thm
    11.8 +        val induct_thm' = Thm.instantiate' [] insts induct_thm
    11.9          val rules = @{thms finite_item.intros}
   11.10        in
   11.11          SOLVED' (fn i => EVERY
    12.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon Jul 27 16:35:12 2015 +0200
    12.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon Jul 27 17:44:55 2015 +0200
    12.3 @@ -1047,7 +1047,7 @@
    12.4            ctxt addsimps @{thms field_simps}
    12.5            addsimps [@{thm nonzero_power_divide}, @{thm power_divide}]
    12.6          val th =
    12.7 -          instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
    12.8 +          Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
    12.9              (if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
   12.10               else @{lemma "(d=0 --> P) & (d ~= (0::real) --> P) ==> P" by blast})
   12.11        in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
    13.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Jul 27 16:35:12 2015 +0200
    13.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Jul 27 17:44:55 2015 +0200
    13.3 @@ -317,7 +317,7 @@
    13.4    | _ => raise CTERM ("find_cterm",[t]);
    13.5  
    13.6      (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
    13.7 -fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
    13.8 +fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
    13.9  fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
   13.10  
   13.11  fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
   13.12 @@ -396,9 +396,9 @@
   13.13      fun add_rule th th' = fconv_rule (arg_conv (oprconv poly_add_conv))
   13.14           (match_mp_rule pth_add [th, th'])
   13.15      fun emul_rule ct th = fconv_rule (arg_conv (oprconv poly_mul_conv))
   13.16 -       (instantiate' [] [SOME ct] (th RS pth_emul))
   13.17 +       (Thm.instantiate' [] [SOME ct] (th RS pth_emul))
   13.18      fun square_rule t = fconv_rule (arg_conv (oprconv poly_conv))
   13.19 -       (instantiate' [] [SOME t] pth_square)
   13.20 +       (Thm.instantiate' [] [SOME t] pth_square)
   13.21  
   13.22      fun hol_of_positivstellensatz(eqs,les,lts) proof =
   13.23        let
   13.24 @@ -444,7 +444,7 @@
   13.25            if c aconvc (concl th2) then ()
   13.26            else error "disj_cases : conclusions not alpha convertible"
   13.27        in Thm.implies_elim (Thm.implies_elim
   13.28 -          (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
   13.29 +          (Thm.implies_elim (Thm.instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
   13.30            (Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
   13.31          (Thm.implies_intr (Thm.apply @{cterm Trueprop} q) th2)
   13.32        end
   13.33 @@ -518,9 +518,9 @@
   13.34          (instantiate_cterm' [SOME (Thm.ctyp_of_cterm x)] [] @{cpat "All :: (?'a => bool) => _" })
   13.35          (Thm.abstract_rule (name_of x) x th)
   13.36  
   13.37 -    val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   13.38 +    val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
   13.39  
   13.40 -    fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   13.41 +    fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
   13.42      fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
   13.43  
   13.44      fun choose v th th' =
   13.45 @@ -530,7 +530,7 @@
   13.46            val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
   13.47            val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
   13.48            val th0 = fconv_rule (Thm.beta_conversion true)
   13.49 -            (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   13.50 +            (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   13.51            val pv = (Thm.rhs_of o Thm.beta_conversion true)
   13.52              (Thm.apply @{cterm Trueprop} (Thm.apply p v))
   13.53            val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
   13.54 @@ -579,7 +579,7 @@
   13.55                  (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
   13.56            in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
   13.57            end
   13.58 -      in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
   13.59 +      in (Thm.implies_elim (Thm.instantiate' [] [SOME ct] pth_final) th, certificates)
   13.60        end
   13.61    in f
   13.62    end;
   13.63 @@ -710,7 +710,7 @@
   13.64                  (eq_pols @ le_pols @ lt_pols) [])
   13.65      val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
   13.66      val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
   13.67 -    val le' = le @ map (fn a => instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens
   13.68 +    val le' = le @ map (fn a => Thm.instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens
   13.69    in ((translator (eq,le',lt) proof), Trivial)
   13.70    end
   13.71  end;
   13.72 @@ -725,9 +725,9 @@
   13.73  
   13.74    val absmaxmin_elim_conv2 =
   13.75      let
   13.76 -      val pth_abs = instantiate' [SOME @{ctyp real}] [] abs_split'
   13.77 -      val pth_max = instantiate' [SOME @{ctyp real}] [] max_split
   13.78 -      val pth_min = instantiate' [SOME @{ctyp real}] [] min_split
   13.79 +      val pth_abs = Thm.instantiate' [SOME @{ctyp real}] [] abs_split'
   13.80 +      val pth_max = Thm.instantiate' [SOME @{ctyp real}] [] max_split
   13.81 +      val pth_min = Thm.instantiate' [SOME @{ctyp real}] [] min_split
   13.82        val abs_tm = @{cterm "abs :: real => _"}
   13.83        val p_v = (("P", 0), @{typ "real \<Rightarrow> bool"})
   13.84        val x_v = (("x", 0), @{typ real})
    14.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Mon Jul 27 16:35:12 2015 +0200
    14.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Mon Jul 27 17:44:55 2015 +0200
    14.3 @@ -154,7 +154,7 @@
    14.4          (Numeral.mk_cnumber @{ctyp "real"} b)
    14.5  end;
    14.6  
    14.7 -fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
    14.8 +fun norm_cmul_rule c th = Thm.instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
    14.9  
   14.10  fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm};
   14.11  
   14.12 @@ -342,7 +342,7 @@
   14.13    val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) []
   14.14    val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
   14.15    val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
   14.16 -  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
   14.17 +  fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
   14.18    fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   14.19    fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   14.20    val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Thm.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns
    15.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Jul 27 16:35:12 2015 +0200
    15.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Jul 27 17:44:55 2015 +0200
    15.3 @@ -110,7 +110,7 @@
    15.4              val dj_cp' = [cp, dj] MRS dj_cp;
    15.5              val cert = SOME o Thm.cterm_of ctxt
    15.6            in
    15.7 -            SOME (mk_meta_eq (Drule.instantiate' [SOME (Thm.ctyp_of ctxt S)]
    15.8 +            SOME (mk_meta_eq (Thm.instantiate' [SOME (Thm.ctyp_of ctxt S)]
    15.9                [cert t, cert r, cert s] dj_cp'))
   15.10            end
   15.11          else NONE
   15.12 @@ -1282,7 +1282,7 @@
   15.13              _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ _)) $ _ => U = T
   15.14            | _ => false)) perm_fresh_fresh
   15.15        in
   15.16 -        Drule.instantiate' []
   15.17 +        Thm.instantiate' []
   15.18            [SOME (Thm.global_cterm_of thy a), NONE, SOME (Thm.global_cterm_of thy b)] th
   15.19        end;
   15.20  
    16.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon Jul 27 16:35:12 2015 +0200
    16.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Jul 27 17:44:55 2015 +0200
    16.3 @@ -203,7 +203,7 @@
    16.4      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    16.5      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    16.6  
    16.7 -    val inductive_forall_def' = Drule.instantiate'
    16.8 +    val inductive_forall_def' = Thm.instantiate'
    16.9        [SOME (Thm.global_ctyp_of thy fsT)] [] inductive_forall_def;
   16.10  
   16.11      fun lift_pred' t (Free (s, T)) ts =
   16.12 @@ -488,7 +488,7 @@
   16.13                           let
   16.14                             val (cf, ct) =
   16.15                               Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th));
   16.16 -                           val arg_cong' = Drule.instantiate'
   16.17 +                           val arg_cong' = Thm.instantiate'
   16.18                               [SOME (Thm.ctyp_of_cterm ct)]
   16.19                               [NONE, SOME ct, SOME cf] (arg_cong RS iffD2);
   16.20                             val inst = Thm.first_order_match (ct,
    17.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Mon Jul 27 16:35:12 2015 +0200
    17.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Jul 27 17:44:55 2015 +0200
    17.3 @@ -227,7 +227,7 @@
    17.4      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    17.5      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    17.6  
    17.7 -    val inductive_forall_def' = Drule.instantiate'
    17.8 +    val inductive_forall_def' = Thm.instantiate'
    17.9        [SOME (Thm.global_ctyp_of thy fsT)] [] inductive_forall_def;
   17.10  
   17.11      fun lift_pred' t (Free (s, T)) ts =
   17.12 @@ -316,7 +316,7 @@
   17.13          val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
   17.14          val fs_atom = Global_Theory.get_thm thy
   17.15            ("fs_" ^ Long_Name.base_name atom ^ "1");
   17.16 -        val avoid_th = Drule.instantiate'
   17.17 +        val avoid_th = Thm.instantiate'
   17.18            [SOME (Thm.global_ctyp_of thy (fastype_of p))] [SOME (Thm.global_cterm_of thy p)]
   17.19            ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
   17.20          val (([(_, cx)], th1 :: th2 :: ths), ctxt') = Obtain.result
    18.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Mon Jul 27 16:35:12 2015 +0200
    18.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Jul 27 17:44:55 2015 +0200
    18.3 @@ -197,13 +197,13 @@
    18.4      in
    18.5        if pi1 <> pi2 then  (* only apply the composition rule in this case *)
    18.6          if T = U then    
    18.7 -          SOME (Drule.instantiate'
    18.8 +          SOME (Thm.instantiate'
    18.9              [SOME (Thm.global_ctyp_of thy (fastype_of t))]
   18.10              [SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
   18.11              (mk_meta_eq ([Global_Theory.get_thm thy ("pt_"^tname'^"_inst"),
   18.12               Global_Theory.get_thm thy ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
   18.13          else
   18.14 -          SOME (Drule.instantiate'
   18.15 +          SOME (Thm.instantiate'
   18.16              [SOME (Thm.global_ctyp_of thy (fastype_of t))]
   18.17              [SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
   18.18              (mk_meta_eq (Global_Theory.get_thm thy ("cp_"^tname'^"_"^uname'^"_inst") RS 
    19.1 --- a/src/HOL/Probability/measurable.ML	Mon Jul 27 16:35:12 2015 +0200
    19.2 +++ b/src/HOL/Probability/measurable.ML	Mon Jul 27 17:44:55 2015 +0200
    19.3 @@ -252,7 +252,7 @@
    19.4            val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
    19.5            fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
    19.6            fun inst (ts, Ts) =
    19.7 -            Drule.instantiate' (cert Thm.global_ctyp_of Ts) (cert Thm.global_cterm_of ts)
    19.8 +            Thm.instantiate' (cert Thm.global_ctyp_of Ts) (cert Thm.global_cterm_of ts)
    19.9                @{thm measurable_compose_countable}
   19.10          in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end
   19.11          handle TERM _ => no_tac) 1)
    20.1 --- a/src/HOL/String.thy	Mon Jul 27 16:35:12 2015 +0200
    20.2 +++ b/src/HOL/String.thy	Mon Jul 27 17:44:55 2015 +0200
    20.3 @@ -253,7 +253,7 @@
    20.4      put_simpset HOL_ss @{context}
    20.5        addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
    20.6    fun mk_code_eqn x y =
    20.7 -    Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
    20.8 +    Thm.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
    20.9      |> simplify simpset;
   20.10    val code_eqns = map_product mk_code_eqn nibbles nibbles;
   20.11  in
    21.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Jul 27 16:35:12 2015 +0200
    21.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Jul 27 17:44:55 2015 +0200
    21.3 @@ -1251,7 +1251,7 @@
    21.4                      map Bound (live - 1 downto 0)) $ Bound live));
    21.5                  val cts = [NONE, SOME (Thm.cterm_of lthy tinst)];
    21.6                in
    21.7 -                Drule.instantiate' cTs cts @{thm surj_imp_ordLeq}
    21.8 +                Thm.instantiate' cTs cts @{thm surj_imp_ordLeq}
    21.9                end);
   21.10              val bd = mk_cexp
   21.11                (if live = 0 then ctwo
    22.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jul 27 16:35:12 2015 +0200
    22.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jul 27 17:44:55 2015 +0200
    22.3 @@ -1838,7 +1838,7 @@
    22.4  
    22.5          val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
    22.6  
    22.7 -        fun mk_case_split' cp = Drule.instantiate' [] [SOME (Thm.cterm_of lthy cp)] @{thm case_split};
    22.8 +        fun mk_case_split' cp = Thm.instantiate' [] [SOME (Thm.cterm_of lthy cp)] @{thm case_split};
    22.9  
   22.10          val case_splitss' = map (map mk_case_split') cpss;
   22.11  
   22.12 @@ -1864,7 +1864,7 @@
   22.13        let
   22.14          val (domT, ranT) = dest_funT (fastype_of sel);
   22.15          val arg_cong' =
   22.16 -          Drule.instantiate' (map (SOME o Thm.ctyp_of lthy) [domT, ranT])
   22.17 +          Thm.instantiate' (map (SOME o Thm.ctyp_of lthy) [domT, ranT])
   22.18              [NONE, NONE, SOME (Thm.cterm_of lthy sel)] arg_cong
   22.19            |> Thm.varifyT_global;
   22.20          val sel_thm' = sel_thm RSN (2, trans);
    23.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jul 27 16:35:12 2015 +0200
    23.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jul 27 17:44:55 2015 +0200
    23.3 @@ -142,7 +142,7 @@
    23.4  fun mk_ctor_iff_dtor_tac ctxt cTs cctor cdtor ctor_dtor dtor_ctor =
    23.5    HEADGOAL (rtac ctxt iffI THEN'
    23.6      EVERY' (@{map 3} (fn cTs => fn cx => fn th =>
    23.7 -      dtac ctxt (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
    23.8 +      dtac ctxt (Thm.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
    23.9        SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN'
   23.10        assume_tac ctxt) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor]));
   23.11  
    24.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jul 27 16:35:12 2015 +0200
    24.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jul 27 17:44:55 2015 +0200
    24.3 @@ -497,7 +497,7 @@
    24.4        val T = mk_tupleT_balanced tfrees;
    24.5      in
    24.6        @{thm asm_rl[of "ALL x. P x --> Q x" for P Q]}
    24.7 -      |> Drule.instantiate' [SOME (Thm.ctyp_of @{context} T)] []
    24.8 +      |> Thm.instantiate' [SOME (Thm.ctyp_of @{context} T)] []
    24.9        |> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]}
   24.10        |> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
   24.11        |> Thm.varifyT_global
    25.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jul 27 16:35:12 2015 +0200
    25.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jul 27 17:44:55 2015 +0200
    25.3 @@ -1975,7 +1975,7 @@
    25.4            in
    25.5              @{map 6} (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
    25.6                ((set_minimal
    25.7 -                |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y')
    25.8 +                |> Thm.instantiate' cTs (mk_induct_tinst phis jsets y y')
    25.9                  |> unfold_thms lthy incls) OF
   25.10                  (replicate n ballI @
   25.11                    maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
   25.12 @@ -2107,7 +2107,7 @@
   25.13              val cphis = @{map 9} mk_cphi
   25.14                Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
   25.15  
   25.16 -            val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
   25.17 +            val coinduct = Thm.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
   25.18  
   25.19              val goal =
   25.20                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    26.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Jul 27 16:35:12 2015 +0200
    26.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Jul 27 17:44:55 2015 +0200
    26.3 @@ -157,7 +157,7 @@
    26.4      let
    26.5        val s = Name.uu;
    26.6        val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
    26.7 -      val split' = Drule.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split;
    26.8 +      val split' = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split;
    26.9      in
   26.10        Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
   26.11      end
    27.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Jul 27 16:35:12 2015 +0200
    27.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Jul 27 17:44:55 2015 +0200
    27.3 @@ -175,7 +175,7 @@
    27.4      rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1;
    27.5  
    27.6  fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs =
    27.7 -  EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
    27.8 +  EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
    27.9      REPEAT_DETERM o rtac ctxt allI,
   27.10      CONJ_WRAP' (fn thm => EVERY'
   27.11        [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm empty_subsetI}]) rec_0s,
   27.12 @@ -195,7 +195,7 @@
   27.13      REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], assume_tac ctxt])) (1 upto n)) 1
   27.14  
   27.15  fun mk_mor_col_tac ctxt m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss =
   27.16 -  EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   27.17 +  EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   27.18      REPEAT_DETERM o rtac ctxt allI,
   27.19      CONJ_WRAP' (fn thm => EVERY' (map (rtac ctxt) [impI, thm RS trans, thm RS sym])) rec_0s,
   27.20      REPEAT_DETERM o rtac ctxt allI,
   27.21 @@ -400,7 +400,7 @@
   27.22      val n = length Lev_0s;
   27.23      val ks = n downto 1;
   27.24    in
   27.25 -    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   27.26 +    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   27.27        REPEAT_DETERM o rtac ctxt allI,
   27.28        CONJ_WRAP' (fn Lev_0 =>
   27.29          EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
   27.30 @@ -425,7 +425,7 @@
   27.31      val n = length rv_Nils;
   27.32      val ks = 1 upto n;
   27.33    in
   27.34 -    EVERY' [rtac ctxt (Drule.instantiate' cTs cts @{thm list.induct}),
   27.35 +    EVERY' [rtac ctxt (Thm.instantiate' cTs cts @{thm list.induct}),
   27.36        REPEAT_DETERM o rtac ctxt allI,
   27.37        CONJ_WRAP' (fn rv_Cons =>
   27.38          CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac ctxt exI,
   27.39 @@ -450,7 +450,7 @@
   27.40      val n = length Lev_0s;
   27.41      val ks = 1 upto n;
   27.42    in
   27.43 -    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   27.44 +    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   27.45        REPEAT_DETERM o rtac ctxt allI,
   27.46        CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
   27.47          EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
   27.48 @@ -496,7 +496,7 @@
   27.49      val n = length Lev_0s;
   27.50      val ks = 1 upto n;
   27.51    in
   27.52 -    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   27.53 +    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   27.54        REPEAT_DETERM o rtac ctxt allI,
   27.55        CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
   27.56          EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
   27.57 @@ -867,7 +867,7 @@
   27.58    let
   27.59      val n = length dtor_maps;
   27.60    in
   27.61 -    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   27.62 +    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   27.63        REPEAT_DETERM o rtac ctxt allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
   27.64        CONJ_WRAP' (K (rtac ctxt @{thm image_empty})) rec_0s,
   27.65        REPEAT_DETERM o rtac ctxt allI,
   27.66 @@ -889,7 +889,7 @@
   27.67    let
   27.68      val n = length rec_0s;
   27.69    in
   27.70 -    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   27.71 +    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   27.72        REPEAT_DETERM o rtac ctxt allI,
   27.73        CONJ_WRAP' (fn rec_0 => EVERY' (map (rtac ctxt) [ordIso_ordLeq_trans,
   27.74          @{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s,
    28.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Jul 27 16:35:12 2015 +0200
    28.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Jul 27 17:44:55 2015 +0200
    28.3 @@ -1581,7 +1581,7 @@
    28.4                (@{map 4} (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
    28.5  
    28.6              val inducts = map (fn cphis =>
    28.7 -              Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
    28.8 +              Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
    28.9  
   28.10              val goals =
   28.11                @{map 3} (fn f => fn sets => fn sets' =>
   28.12 @@ -1610,7 +1610,7 @@
   28.13              val cphiss = map (map2 mk_cphi Izs) Isetss_by_range;
   28.14  
   28.15              val inducts = map (fn cphis =>
   28.16 -              Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
   28.17 +              Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
   28.18  
   28.19              val goals =
   28.20                map (fn sets =>
   28.21 @@ -1645,7 +1645,7 @@
   28.22  
   28.23              val cphis = @{map 4} mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
   28.24  
   28.25 -            val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
   28.26 +            val induct = Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
   28.27  
   28.28              val goal =
   28.29                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   28.30 @@ -1706,7 +1706,7 @@
   28.31              val cxs = map (SOME o Thm.cterm_of lthy) (splice Izs1 Izs2);
   28.32              fun mk_cphi z1 z2 goal = SOME (Thm.cterm_of lthy (Term.absfree z1 (Term.absfree z2 goal)));
   28.33              val cphis = @{map 3} mk_cphi Izs1' Izs2' goals;
   28.34 -            val induct = Drule.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
   28.35 +            val induct = Thm.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
   28.36  
   28.37              val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
   28.38            in
    29.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Jul 27 16:35:12 2015 +0200
    29.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Jul 27 17:44:55 2015 +0200
    29.3 @@ -222,7 +222,7 @@
    29.4    suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite =
    29.5    let
    29.6      val induct = worel RS
    29.7 -      Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
    29.8 +      Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
    29.9      val src = 1 upto m + 1;
   29.10      val dest = (m + 1) :: (1 upto m);
   29.11      val absorbAs_tac = if m = 0 then K (all_tac)
   29.12 @@ -268,7 +268,7 @@
   29.13  fun mk_min_algs_least_tac ctxt cT ct worel min_algs alg_sets =
   29.14    let
   29.15      val induct = worel RS
   29.16 -      Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
   29.17 +      Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
   29.18  
   29.19      val minG_tac =
   29.20        EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E},
   29.21 @@ -444,7 +444,7 @@
   29.22  fun mk_mor_fold_tac ctxt cT ct fold_defs ex_mor mor =
   29.23    (EVERY' (map (stac ctxt) fold_defs) THEN' EVERY' [rtac ctxt rev_mp, rtac ctxt ex_mor, rtac ctxt impI] THEN'
   29.24    REPEAT_DETERM_N (length fold_defs) o etac ctxt exE THEN'
   29.25 -  rtac ctxt (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1;
   29.26 +  rtac ctxt (Thm.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1;
   29.27  
   29.28  fun mk_fold_unique_mor_tac ctxt type_defs init_unique_mors Reps mor_comp mor_Abs mor_fold =
   29.29    let
   29.30 @@ -515,7 +515,7 @@
   29.31              assume_tac ctxt],
   29.32          assume_tac ctxt];
   29.33    in
   29.34 -    EVERY' [rtac ctxt rev_mp, rtac ctxt (Drule.instantiate' cTs cts ctor_induct),
   29.35 +    EVERY' [rtac ctxt rev_mp, rtac ctxt (Thm.instantiate' cTs cts ctor_induct),
   29.36        EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac ctxt impI,
   29.37        REPEAT_DETERM o eresolve_tac ctxt [conjE, allE],
   29.38        CONJ_WRAP' (K (assume_tac ctxt)) ks] 1
    30.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jul 27 16:35:12 2015 +0200
    30.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jul 27 17:44:55 2015 +0200
    30.3 @@ -690,7 +690,7 @@
    30.4              (map Logic.varifyT_global As ~~ As);
    30.5  
    30.6          fun inst_thm t thm =
    30.7 -          Drule.instantiate' [] [SOME (Thm.cterm_of lthy t)]
    30.8 +          Thm.instantiate' [] [SOME (Thm.cterm_of lthy t)]
    30.9              (Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm));
   30.10  
   30.11          val uexhaust_thm = inst_thm u exhaust_thm;
    31.1 --- a/src/HOL/Tools/Function/function_context_tree.ML	Mon Jul 27 16:35:12 2015 +0200
    31.2 +++ b/src/HOL/Tools/Function/function_context_tree.ML	Mon Jul 27 17:44:55 2015 +0200
    31.3 @@ -248,7 +248,7 @@
    31.4            val iha = import_thm ctxt (fix, h_as) ha (* (a', h a') : G *)
    31.5              |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
    31.6                                                      (* (a, h a) : G   *)
    31.7 -          val inst_ih = instantiate' [] [SOME (Thm.cterm_of ctxt arg)] ih
    31.8 +          val inst_ih = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt arg)] ih
    31.9            val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
   31.10  
   31.11            val h_a'_eq_h_a = Thm.combination (Thm.reflexive (Thm.cterm_of ctxt h)) inner
    32.1 --- a/src/HOL/Tools/Function/function_core.ML	Mon Jul 27 16:35:12 2015 +0200
    32.2 +++ b/src/HOL/Tools/Function/function_core.ML	Mon Jul 27 17:44:55 2015 +0200
    32.3 @@ -371,7 +371,7 @@
    32.4  
    32.5      val exactly_one =
    32.6        @{thm ex1I}
    32.7 -      |> instantiate'
    32.8 +      |> Thm.instantiate'
    32.9            [SOME (Thm.ctyp_of ctxt ranT)]
   32.10            [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
   32.11        |> curry (op COMP) existence
   32.12 @@ -407,7 +407,7 @@
   32.13      val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
   32.14      val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
   32.15      val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
   32.16 -      |> instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
   32.17 +      |> Thm.instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
   32.18  
   32.19      val _ = trace_msg (K "Proving Replacement lemmas...")
   32.20      val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses
   32.21 @@ -694,7 +694,7 @@
   32.22        |> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
   32.23        |> assume_tac ctxt 1 |> Seq.hd
   32.24        |> (curry op COMP) (acc_downward
   32.25 -        |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
   32.26 +        |> (Thm.instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
   32.27          |> Thm.forall_intr (Thm.cterm_of ctxt z)
   32.28          |> Thm.forall_intr (Thm.cterm_of ctxt x))
   32.29        |> Thm.forall_intr (Thm.cterm_of ctxt a)
    33.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Mon Jul 27 16:35:12 2015 +0200
    33.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Mon Jul 27 17:44:55 2015 +0200
    33.3 @@ -374,7 +374,7 @@
    33.4            |> Thm.cterm_of ctxt''
    33.5        in
    33.6          indthm
    33.7 -        |> Drule.instantiate' [] [SOME inst]
    33.8 +        |> Thm.instantiate' [] [SOME inst]
    33.9          |> simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt'')
   33.10          |> Conv.fconv_rule (ind_rulify ctxt'')
   33.11        end
    34.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Mon Jul 27 16:35:12 2015 +0200
    34.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Mon Jul 27 17:44:55 2015 +0200
    34.3 @@ -278,7 +278,7 @@
    34.4           THEN (resolve_tac ctxt @{thms reduction_pair_lemma} 1)
    34.5           THEN (resolve_tac ctxt @{thms rp_inv_image_rp} 1)
    34.6           THEN (resolve_tac ctxt [order_rpair ms_rp label] 1)
    34.7 -         THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
    34.8 +         THEN PRIMITIVE (Thm.instantiate' [] [SOME level_mapping])
    34.9           THEN unfold_tac ctxt @{thms rp_inv_image_def}
   34.10           THEN Local_Defs.unfold_tac ctxt @{thms split_conv fst_conv snd_conv}
   34.11           THEN REPEAT (SOMEGOAL (resolve_tac ctxt [@{thm Un_least}, @{thm empty_subsetI}]))
    35.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon Jul 27 16:35:12 2015 +0200
    35.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Mon Jul 27 17:44:55 2015 +0200
    35.3 @@ -409,7 +409,7 @@
    35.4        then 
    35.5          let 
    35.6            val instantiated_id_quot_thm =
    35.7 -            instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
    35.8 +            Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
    35.9          in
   35.10            (instantiated_id_quot_thm, (table, ctxt)) 
   35.11          end
    36.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon Jul 27 16:35:12 2015 +0200
    36.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Jul 27 17:44:55 2015 +0200
    36.3 @@ -173,7 +173,7 @@
    36.4      let
    36.5        val cc = Thm.cterm_of ctxt c
    36.6        val ct = Thm.dest_arg (Thm.cprop_of th)
    36.7 -    in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    36.8 +    in resolve_tac ctxt [th] i (Thm.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    36.9    | _ => resolve_tac ctxt [th] i st
   36.10  
   36.11  (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
    37.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon Jul 27 16:35:12 2015 +0200
    37.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Mon Jul 27 17:44:55 2015 +0200
    37.3 @@ -102,13 +102,13 @@
    37.4        val cxT = Thm.ctyp_of ctxt xT
    37.5        val cbodyT = Thm.ctyp_of ctxt bodyT
    37.6        fun makeK () =
    37.7 -        instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.cterm_of ctxt body)] @{thm abs_K}
    37.8 +        Thm.instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.cterm_of ctxt body)] @{thm abs_K}
    37.9    in
   37.10        case body of
   37.11            Const _ => makeK()
   37.12          | Free _ => makeK()
   37.13          | Var _ => makeK()  (*though Var isn't expected*)
   37.14 -        | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
   37.15 +        | Bound 0 => Thm.instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
   37.16          | rator$rand =>
   37.17              if Term.is_dependent rator then (*C or S*)
   37.18                 if Term.is_dependent rand then (*S*)
    38.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jul 27 16:35:12 2015 +0200
    38.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jul 27 17:44:55 2015 +0200
    38.3 @@ -50,7 +50,7 @@
    38.4      let
    38.5        val ct = Thm.cterm_of ctxt t
    38.6        val cT = Thm.ctyp_of_cterm ct
    38.7 -    in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
    38.8 +    in refl |> Thm.instantiate' [SOME cT] [SOME ct] end
    38.9    | Const (@{const_name disj}, _) $ t1 $ t2 =>
   38.10      (if can HOLogic.dest_not t1 then t2 else t1)
   38.11      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
    39.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Jul 27 16:35:12 2015 +0200
    39.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Jul 27 17:44:55 2015 +0200
    39.3 @@ -397,7 +397,7 @@
    39.4      (* prove  inj Rep_dt_i  and  Rep_dt_i x : rep_set_dt_i *)
    39.5  
    39.6      val fun_congs =
    39.7 -      map (fn T => make_elim (Drule.instantiate' [SOME (Thm.global_ctyp_of thy5 T)] [] fun_cong)) branchTs;
    39.8 +      map (fn T => make_elim (Thm.instantiate' [SOME (Thm.global_ctyp_of thy5 T)] [] fun_cong)) branchTs;
    39.9  
   39.10      fun prove_iso_thms ds (inj_thms, elem_thms) =
   39.11        let
    40.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Jul 27 16:35:12 2015 +0200
    40.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Jul 27 17:44:55 2015 +0200
    40.3 @@ -84,17 +84,17 @@
    40.4  val is_number = can dest_number;
    40.5  
    40.6  val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
    40.7 -    map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
    40.8 +    map (Thm.instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
    40.9  
   40.10  val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =
   40.11 -    map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
   40.12 +    map (Thm.instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
   40.13  
   40.14  val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] =
   40.15 -    map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
   40.16 +    map (Thm.instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
   40.17  
   40.18 -val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
   40.19 +val [miP, piP] = map (Thm.instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
   40.20  
   40.21 -val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
   40.22 +val infDP = Thm.instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
   40.23  
   40.24  val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,
   40.25        asetgt, asetge, asetdvd, asetndvd,asetP],
   40.26 @@ -103,7 +103,7 @@
   40.27  
   40.28  val [cpmi, cppi] = [@{thm "cpmi"}, @{thm "cppi"}];
   40.29  
   40.30 -val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
   40.31 +val unity_coeff_ex = Thm.instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
   40.32  
   40.33  val [zdvd_mono,simp_from_to,all_not_ex] =
   40.34       [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
   40.35 @@ -166,9 +166,9 @@
   40.36    in (mi_th, set_th, infD_th)
   40.37    end;
   40.38  
   40.39 -val inst' = fn cts => instantiate' [] (map SOME cts);
   40.40 -val infDTrue = instantiate' [] [SOME true_tm] infDP;
   40.41 -val infDFalse = instantiate' [] [SOME false_tm] infDP;
   40.42 +val inst' = fn cts => Thm.instantiate' [] (map SOME cts);
   40.43 +val infDTrue = Thm.instantiate' [] [SOME true_tm] infDP;
   40.44 +val infDFalse = Thm.instantiate' [] [SOME false_tm] infDP;
   40.45  
   40.46  val cadd =  @{cterm "op + :: int => _"}
   40.47  val cmulC =  @{cterm "op * :: int => _"}
   40.48 @@ -483,16 +483,16 @@
   40.49     in Thm.equal_elim (Thm.symmetric th) TrueI end;
   40.50      (* A and B set *)
   40.51     local
   40.52 -     val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
   40.53 -     val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
   40.54 +     val insI1 = Thm.instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
   40.55 +     val insI2 = Thm.instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
   40.56     in
   40.57      fun provein x S =
   40.58       case Thm.term_of S of
   40.59          Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
   40.60        | Const(@{const_name insert}, _) $ y $ _ =>
   40.61           let val (cy,S') = Thm.dest_binop S
   40.62 -         in if Thm.term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
   40.63 -         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   40.64 +         in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1
   40.65 +         else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   40.66                             (provein x S')
   40.67           end
   40.68     end
   40.69 @@ -519,7 +519,7 @@
   40.70    let
   40.71     val sths = map (fn (tl,t0) =>
   40.72                        if tl = Thm.term_of t0
   40.73 -                      then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
   40.74 +                      then Thm.instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
   40.75                        else provelin ctxt ((HOLogic.eq_const iT)$tl$(Thm.term_of t0)
   40.76                                   |> HOLogic.mk_Trueprop))
   40.77                     (sl ~~ s0)
   40.78 @@ -527,7 +527,7 @@
   40.79     val S = mkISet csl
   40.80     val inStab = fold (fn ct => fn tab => Termtab.update (Thm.term_of ct, provein ct S) tab)
   40.81                      csl Termtab.empty
   40.82 -   val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
   40.83 +   val eqelem_th = Thm.instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
   40.84     val inS =
   40.85       let
   40.86        val tab = fold Termtab.update
   40.87 @@ -536,7 +536,7 @@
   40.88                      val th =
   40.89                        if s aconvc t
   40.90                        then the (Termtab.lookup inStab (Thm.term_of s))
   40.91 -                      else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
   40.92 +                      else FWD (Thm.instantiate' [] [SOME s, SOME t] eqelem_th)
   40.93                          [eq, the (Termtab.lookup inStab (Thm.term_of s))]
   40.94                   in (Thm.term_of t, th) end) sths) Termtab.empty
   40.95          in
   40.96 @@ -801,7 +801,7 @@
   40.97  
   40.98  fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
   40.99   let 
  40.100 -   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
  40.101 +   fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"}
  40.102     fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
  40.103     val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
  40.104     val p' = fold_rev gen ts p
    41.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Mon Jul 27 16:35:12 2015 +0200
    41.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Mon Jul 27 17:44:55 2015 +0200
    41.3 @@ -45,7 +45,7 @@
    41.4      let
    41.5       val p = Thm.dest_arg p
    41.6       val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
    41.7 -     val th = instantiate' [SOME T] [SOME p] all_not_ex
    41.8 +     val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex
    41.9      in Thm.transitive th (conv env (Thm.rhs_of th))
   41.10      end
   41.11    | _ => atcv env p
    42.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 27 16:35:12 2015 +0200
    42.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 27 17:44:55 2015 +0200
    42.3 @@ -80,7 +80,7 @@
    42.4      val cty = Thm.global_ctyp_of thy ty;
    42.5    in
    42.6      @{thm partial_term_of_anything}
    42.7 -    |> Drule.instantiate' [SOME cty] insts
    42.8 +    |> Thm.instantiate' [SOME cty] insts
    42.9      |> Thm.varifyT_global
   42.10    end
   42.11  
   42.12 @@ -99,7 +99,7 @@
   42.13            @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
   42.14      val var_eq =
   42.15        @{thm partial_term_of_anything}
   42.16 -      |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
   42.17 +      |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
   42.18        |> Thm.varifyT_global
   42.19      val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs;
   42.20   in
    43.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Jul 27 16:35:12 2015 +0200
    43.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Jul 27 17:44:55 2015 +0200
    43.3 @@ -99,7 +99,7 @@
    43.4      val ty_inst = map (SOME o Thm.ctyp_of ctxt) [domain_type (fastype_of R2)]
    43.5      val trm_inst = map (SOME o Thm.cterm_of ctxt) [R2, R1]
    43.6    in
    43.7 -    (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
    43.8 +    (case try (Thm.instantiate' ty_inst trm_inst) ball_bex_thm of
    43.9        NONE => NONE
   43.10      | SOME thm' =>
   43.11          (case try (get_match_inst thy (get_lhs thm')) redex of
   43.12 @@ -198,7 +198,7 @@
   43.13          val cfx = Thm.cterm_of ctxt fx;
   43.14          val cxt = Thm.ctyp_of ctxt (fastype_of x);
   43.15          val cfxt = Thm.ctyp_of ctxt (fastype_of fx);
   43.16 -        val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
   43.17 +        val thm = Thm.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
   43.18        in
   43.19          Conv.rewr_conv thm ctrm
   43.20        end)
   43.21 @@ -247,7 +247,7 @@
   43.22                val ty_f = range_type (fastype_of f)
   43.23                val ty_inst = map (SOME o Thm.ctyp_of ctxt) [ty_x, ty_b, ty_f]
   43.24                val t_inst = map (SOME o Thm.cterm_of ctxt) [R2, f, g, x, y];
   43.25 -              val inst_thm = Drule.instantiate' ty_inst
   43.26 +              val inst_thm = Thm.instantiate' ty_inst
   43.27                  ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
   43.28              in
   43.29                (resolve_tac ctxt [inst_thm] THEN' SOLVED' (quotient_tac ctxt)) 1
   43.30 @@ -264,7 +264,7 @@
   43.31        let
   43.32          val ty = domain_type (fastype_of R)
   43.33        in
   43.34 -        case try (Drule.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
   43.35 +        case try (Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
   43.36              [SOME (Thm.cterm_of ctxt R)]) @{thm equals_rsp} of
   43.37            SOME thm => resolve_tac ctxt [thm] THEN' quotient_tac ctxt
   43.38          | NONE => K no_tac
   43.39 @@ -281,7 +281,7 @@
   43.40          in
   43.41            case try (map (SOME o Thm.cterm_of ctxt)) [rel, abs, rep] of
   43.42              SOME t_inst =>
   43.43 -              (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
   43.44 +              (case try (Thm.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
   43.45                  SOME inst_thm => (resolve_tac ctxt [inst_thm] THEN' quotient_tac ctxt) i
   43.46                | NONE => no_tac)
   43.47            | NONE => no_tac
   43.48 @@ -468,7 +468,7 @@
   43.49          val (ty_c, ty_d) = dest_funT (fastype_of a2)
   43.50          val tyinst = map (SOME o Thm.ctyp_of ctxt) [ty_a, ty_b, ty_c, ty_d]
   43.51          val tinst = [NONE, NONE, SOME (Thm.cterm_of ctxt r1), NONE, SOME (Thm.cterm_of ctxt a2)]
   43.52 -        val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
   43.53 +        val thm1 = Thm.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
   43.54          val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
   43.55          val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
   43.56          val (insp, inst) =
   43.57 @@ -529,7 +529,7 @@
   43.58  (* Tactic for Generalising Free Variables in a Goal *)
   43.59  
   43.60  fun inst_spec ctrm =
   43.61 -  Drule.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec}
   43.62 +  Thm.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec}
   43.63  
   43.64  fun inst_spec_tac ctxt ctrms =
   43.65    EVERY' (map (dresolve_tac ctxt o single o inst_spec) ctrms)
   43.66 @@ -602,7 +602,7 @@
   43.67      val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
   43.68        handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   43.69    in
   43.70 -    Drule.instantiate' []
   43.71 +    Thm.instantiate' []
   43.72        [SOME (Thm.cterm_of ctxt rtrm'),
   43.73         SOME (Thm.cterm_of ctxt reg_goal),
   43.74         NONE,
   43.75 @@ -661,7 +661,7 @@
   43.76      val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
   43.77        handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   43.78    in
   43.79 -    Drule.instantiate' []
   43.80 +    Thm.instantiate' []
   43.81        [SOME (Thm.cterm_of ctxt reg_goal),
   43.82         NONE,
   43.83         SOME (Thm.cterm_of ctxt inj_goal)] partiality_procedure_thm
    44.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Mon Jul 27 16:35:12 2015 +0200
    44.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Mon Jul 27 17:44:55 2015 +0200
    44.3 @@ -218,7 +218,7 @@
    44.4  fun Rel_conv ct =
    44.5    let val (cT, cT') = dest_funcT (Thm.ctyp_of_cterm ct)
    44.6        val (cU, _) = dest_funcT cT'
    44.7 -  in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
    44.8 +  in Thm.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
    44.9  
   44.10  (* Conversion to preprocess a transfer rule *)
   44.11  fun safe_Rel_conv ct =
   44.12 @@ -463,7 +463,7 @@
   44.13              val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
   44.14              val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
   44.15              val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
   44.16 -            val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
   44.17 +            val rule = Thm.instantiate' tinsts insts @{thm Rel_abs}
   44.18              val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
   44.19            in
   44.20              (thm2 COMP rule, hyps)
    45.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Jul 27 16:35:12 2015 +0200
    45.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Jul 27 17:44:55 2015 +0200
    45.3 @@ -359,7 +359,7 @@
    45.4          val kill_True = Local_Defs.unfold lthy [@{thm HOL.simp_thms(21)}]
    45.5        in
    45.6          thm
    45.7 -        |> Drule.instantiate' cTs cts
    45.8 +        |> Thm.instantiate' cTs cts
    45.9          |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
   45.10            (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
   45.11          |> Local_Defs.unfold lthy eq_onps
    46.1 --- a/src/HOL/Tools/choice_specification.ML	Mon Jul 27 16:35:12 2015 +0200
    46.2 +++ b/src/HOL/Tools/choice_specification.ML	Mon Jul 27 17:44:55 2015 +0200
    46.3 @@ -138,7 +138,7 @@
    46.4            let
    46.5              val cv = Thm.global_cterm_of thy v
    46.6              val cT = Thm.ctyp_of_cterm cv
    46.7 -            val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec
    46.8 +            val spec' = Thm.instantiate' [SOME cT] [NONE, SOME cv] spec
    46.9            in thm RS spec' end
   46.10          fun remove_alls frees (thm, thy) = (fold (inst_all thy) frees thm, thy)
   46.11          fun process_single ((name, atts), rew_imp, frees) args =
    47.1 --- a/src/HOL/Tools/cnf.ML	Mon Jul 27 16:35:12 2015 +0200
    47.2 +++ b/src/HOL/Tools/cnf.ML	Mon Jul 27 17:44:55 2015 +0200
    47.3 @@ -165,7 +165,7 @@
    47.4  (* ------------------------------------------------------------------------- *)
    47.5  
    47.6  fun inst_thm thy ts thm =
    47.7 -  instantiate' [] (map (SOME o Thm.global_cterm_of thy) ts) thm;
    47.8 +  Thm.instantiate' [] (map (SOME o Thm.global_cterm_of thy) ts) thm;
    47.9  
   47.10  (* ------------------------------------------------------------------------- *)
   47.11  (*                         Naive CNF transformation                          *)
    48.1 --- a/src/HOL/Tools/code_evaluation.ML	Mon Jul 27 16:35:12 2015 +0200
    48.2 +++ b/src/HOL/Tools/code_evaluation.ML	Mon Jul 27 17:44:55 2015 +0200
    48.3 @@ -69,7 +69,7 @@
    48.4      val cty = Thm.global_ctyp_of thy ty;
    48.5    in
    48.6      @{thm term_of_anything}
    48.7 -    |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    48.8 +    |> Thm.instantiate' [SOME cty] [SOME arg, SOME rhs]
    48.9      |> Thm.varifyT_global
   48.10    end;
   48.11  
   48.12 @@ -106,7 +106,7 @@
   48.13      val cty = Thm.global_ctyp_of thy ty;
   48.14    in
   48.15      @{thm term_of_anything}
   48.16 -    |> Drule.instantiate' [SOME cty] [SOME (Thm.global_cterm_of thy arg), SOME rhs]
   48.17 +    |> Thm.instantiate' [SOME cty] [SOME (Thm.global_cterm_of thy arg), SOME rhs]
   48.18      |> Thm.varifyT_global
   48.19    end;
   48.20  
    49.1 --- a/src/HOL/Tools/groebner.ML	Mon Jul 27 16:35:12 2015 +0200
    49.2 +++ b/src/HOL/Tools/groebner.ML	Mon Jul 27 17:44:55 2015 +0200
    49.3 @@ -413,7 +413,7 @@
    49.4  fun initial_conv ctxt =
    49.5    Simplifier.rewrite (put_simpset initial_ss ctxt);
    49.6  
    49.7 -val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
    49.8 +val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
    49.9  
   49.10  val cTrp = @{cterm "Trueprop"};
   49.11  val cConj = @{cterm HOL.conj};
   49.12 @@ -435,7 +435,7 @@
   49.13  
   49.14  fun sym_conv eq =
   49.15   let val (l,r) = Thm.dest_binop eq
   49.16 - in instantiate' [SOME (Thm.ctyp_of_cterm l)] [SOME l, SOME r] eq_commute
   49.17 + in Thm.instantiate' [SOME (Thm.ctyp_of_cterm l)] [SOME l, SOME r] eq_commute
   49.18   end;
   49.19  
   49.20    (* FIXME : copied from cqe.ML -- complex QE*)
   49.21 @@ -471,14 +471,14 @@
   49.22    fun tabr c = the (Termtab.lookup ctabr (Thm.term_of c))
   49.23    val thl  = prove_conj tabl (conjuncts r) |> implies_intr_hyps
   49.24    val thr  = prove_conj tabr (conjuncts l) |> implies_intr_hyps
   49.25 -  val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI}
   49.26 +  val eqI = Thm.instantiate' [] [SOME l, SOME r] @{thm iffI}
   49.27   in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
   49.28  
   49.29   (* END FIXME.*)
   49.30  
   49.31     (* Conversion for the equivalence of existential statements where
   49.32        EX quantifiers are rearranged differently *)
   49.33 - fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   49.34 + fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
   49.35   fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
   49.36  
   49.37  fun choose v th th' = case Thm.concl_of th of
   49.38 @@ -487,7 +487,7 @@
   49.39      val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
   49.40      val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
   49.41      val th0 = Conv.fconv_rule (Thm.beta_conversion true)
   49.42 -        (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   49.43 +        (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   49.44      val pv = (Thm.rhs_of o Thm.beta_conversion true)
   49.45            (Thm.apply @{cterm Trueprop} (Thm.apply p v))
   49.46      val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
   49.47 @@ -504,7 +504,7 @@
   49.48     val p = Thm.lambda v (Thm.dest_arg (Thm.cprop_of th))
   49.49    in Thm.implies_elim
   49.50      (Conv.fconv_rule (Thm.beta_conversion true)
   49.51 -      (instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI}))
   49.52 +      (Thm.instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI}))
   49.53        th
   49.54    end
   49.55   fun ex_eq_conv t =
   49.56 @@ -517,7 +517,7 @@
   49.57     val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th))
   49.58     val p = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) th1
   49.59     val q = (Thm.dest_arg o Thm.dest_arg o Thm.cprop_of) th1
   49.60 -  in Thm.implies_elim (Thm.implies_elim (instantiate' [] [SOME p, SOME q] iffI) th1) th2
   49.61 +  in Thm.implies_elim (Thm.implies_elim (Thm.instantiate' [] [SOME p, SOME q] iffI) th1) th2
   49.62       |> mk_meta_eq
   49.63    end;
   49.64  
   49.65 @@ -739,7 +739,7 @@
   49.66   let
   49.67    fun mk_forall x p =
   49.68      Thm.apply
   49.69 -      (Drule.cterm_rule (instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
   49.70 +      (Drule.cterm_rule (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
   49.71          @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
   49.72    val avs = Thm.add_cterm_frees tm []
   49.73    val P' = fold mk_forall avs tm
   49.74 @@ -775,7 +775,7 @@
   49.75  fun poly_eq_conv t =
   49.76   let val (a,b) = Thm.dest_binop t
   49.77   in Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv ring_normalize_conv))
   49.78 -     (instantiate' [] [SOME a, SOME b] idl_sub)
   49.79 +     (Thm.instantiate' [] [SOME a, SOME b] idl_sub)
   49.80   end
   49.81   val poly_eq_simproc =
   49.82    let
   49.83 @@ -810,7 +810,7 @@
   49.84     | NONE => (the (find_first
   49.85            (fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th)
   49.86     val th2 = Thm.transitive th1
   49.87 -        (instantiate' []  [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v]
   49.88 +        (Thm.instantiate' []  [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v]
   49.89            idl_add0)
   49.90     in Conv.fconv_rule(funpow 2 Conv.arg_conv ring_normalize_conv) th2
   49.91     end
   49.92 @@ -946,7 +946,7 @@
   49.93   | _=> raise CTERM ("ideal_tac - lhs",[t])
   49.94   fun exitac _ NONE = no_tac
   49.95     | exitac ctxt (SOME y) =
   49.96 -      resolve_tac ctxt [instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1
   49.97 +      resolve_tac ctxt [Thm.instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1
   49.98  
   49.99   val claset = claset_of @{context}
  49.100  in
    50.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Jul 27 16:35:12 2015 +0200
    50.2 +++ b/src/HOL/Tools/inductive_set.ML	Mon Jul 27 17:44:55 2015 +0200
    50.3 @@ -42,7 +42,7 @@
    50.4      let
    50.5        fun close p t f =
    50.6          let val vs = Term.add_vars t []
    50.7 -        in Drule.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
    50.8 +        in Thm.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
    50.9            (p (fold (Logic.all o Var) vs t) f)
   50.10          end;
   50.11        fun mkop @{const_name HOL.conj} T x =
    51.1 --- a/src/HOL/Tools/int_arith.ML	Mon Jul 27 16:35:12 2015 +0200
    51.2 +++ b/src/HOL/Tools/int_arith.ML	Mon Jul 27 17:44:55 2015 +0200
    51.3 @@ -27,7 +27,7 @@
    51.4  fun proc0 phi ctxt ct =
    51.5    let val T = Thm.ctyp_of_cterm ct
    51.6    in if Thm.typ_of T = @{typ int} then NONE else
    51.7 -     SOME (instantiate' [SOME T] [] zeroth)
    51.8 +     SOME (Thm.instantiate' [SOME T] [] zeroth)
    51.9    end;
   51.10  
   51.11  val zero_to_of_int_zero_simproc =
   51.12 @@ -41,7 +41,7 @@
   51.13  fun proc1 phi ctxt ct =
   51.14    let val T = Thm.ctyp_of_cterm ct
   51.15    in if Thm.typ_of T = @{typ int} then NONE else
   51.16 -     SOME (instantiate' [SOME T] [] oneth)
   51.17 +     SOME (Thm.instantiate' [SOME T] [] oneth)
   51.18    end;
   51.19  
   51.20  val one_to_of_int_one_simproc =
    52.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Mon Jul 27 16:35:12 2015 +0200
    52.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Jul 27 17:44:55 2015 +0200
    52.3 @@ -610,7 +610,7 @@
    52.4      val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z,w]
    52.5      val T = Thm.ctyp_of_cterm x
    52.6      val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z]
    52.7 -    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
    52.8 +    val th = Thm.instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
    52.9    in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz)
   52.10    end
   52.11    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
   52.12 @@ -624,13 +624,13 @@
   52.13          let val (x,y) = Thm.dest_binop l val z = r
   52.14              val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
   52.15              val ynz = prove_nz ctxt T y
   52.16 -        in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
   52.17 +        in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
   52.18          end
   52.19       | (_, Const (@{const_name Rings.divide},_)$_$_) =>
   52.20          let val (x,y) = Thm.dest_binop r val z = l
   52.21              val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
   52.22              val ynz = prove_nz ctxt T y
   52.23 -        in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
   52.24 +        in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
   52.25          end
   52.26       | _ => NONE)
   52.27    end
   52.28 @@ -648,42 +648,42 @@
   52.29          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   52.30          val _ = map is_number [a,b,c]
   52.31          val T = Thm.ctyp_of_cterm c
   52.32 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
   52.33 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
   52.34        in SOME (mk_meta_eq th) end
   52.35    | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   52.36        let
   52.37          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   52.38          val _ = map is_number [a,b,c]
   52.39          val T = Thm.ctyp_of_cterm c
   52.40 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
   52.41 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
   52.42        in SOME (mk_meta_eq th) end
   52.43    | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   52.44        let
   52.45          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   52.46          val _ = map is_number [a,b,c]
   52.47          val T = Thm.ctyp_of_cterm c
   52.48 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
   52.49 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
   52.50        in SOME (mk_meta_eq th) end
   52.51    | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   52.52      let
   52.53        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   52.54          val _ = map is_number [a,b,c]
   52.55          val T = Thm.ctyp_of_cterm c
   52.56 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
   52.57 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
   52.58        in SOME (mk_meta_eq th) end
   52.59    | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   52.60      let
   52.61        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   52.62          val _ = map is_number [a,b,c]
   52.63          val T = Thm.ctyp_of_cterm c
   52.64 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   52.65 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   52.66        in SOME (mk_meta_eq th) end
   52.67    | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   52.68      let
   52.69        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   52.70          val _ = map is_number [a,b,c]
   52.71          val T = Thm.ctyp_of_cterm c
   52.72 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
   52.73 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
   52.74        in SOME (mk_meta_eq th) end
   52.75    | _ => NONE)
   52.76    handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
    53.1 --- a/src/HOL/Tools/record.ML	Mon Jul 27 16:35:12 2015 +0200
    53.2 +++ b/src/HOL/Tools/record.ML	Mon Jul 27 17:44:55 2015 +0200
    53.3 @@ -85,7 +85,7 @@
    53.4    let
    53.5      val exists_thm =
    53.6        UNIV_I
    53.7 -      |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type))] [];
    53.8 +      |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type))] [];
    53.9      val proj_constr = Abs_inverse OF [exists_thm];
   53.10      val absT = Type (tyco, map TFree vs);
   53.11    in
    54.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Mon Jul 27 16:35:12 2015 +0200
    54.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Mon Jul 27 17:44:55 2015 +0200
    54.3 @@ -142,7 +142,7 @@
    54.4        let val (a, b) = Rat.quotient_of_rat x
    54.5        in if b = 1 then Numeral.mk_cnumber cT a
    54.6          else Thm.apply
    54.7 -             (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
    54.8 +             (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"})
    54.9                           (Numeral.mk_cnumber cT a))
   54.10               (Numeral.mk_cnumber cT b)
   54.11        end
    55.1 --- a/src/Pure/axclass.ML	Mon Jul 27 16:35:12 2015 +0200
    55.2 +++ b/src/Pure/axclass.ML	Mon Jul 27 17:44:55 2015 +0200
    55.3 @@ -191,7 +191,7 @@
    55.4                thy2
    55.5                |> update_classrel ((c1, c2),
    55.6                  (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
    55.7 -                |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
    55.8 +                |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
    55.9                  |> Thm.close_derivation));
   55.10  
   55.11          val proven = is_classrel thy1;
   55.12 @@ -234,7 +234,7 @@
   55.13        let
   55.14          val th1 =
   55.15            (th RS the_classrel thy (c, c1))
   55.16 -          |> Drule.instantiate' std_vars []
   55.17 +          |> Thm.instantiate' std_vars []
   55.18            |> Thm.close_derivation;
   55.19        in ((th1, thy_name), c1) end);
   55.20  
   55.21 @@ -396,7 +396,7 @@
   55.22      val (th', thy') = Global_Theory.store_thm (binding, th) thy;
   55.23      val th'' = th'
   55.24        |> Thm.unconstrainT
   55.25 -      |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
   55.26 +      |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
   55.27    in
   55.28      thy'
   55.29      |> Sign.primitive_classrel (c1, c2)
   55.30 @@ -426,7 +426,7 @@
   55.31        |> (map o apsnd o map_atyps) (K T);
   55.32      val th'' = th'
   55.33        |> Thm.unconstrainT
   55.34 -      |> Drule.instantiate' std_vars [];
   55.35 +      |> Thm.instantiate' std_vars [];
   55.36    in
   55.37      thy'
   55.38      |> fold (#2 oo declare_overloaded) missing_params
    56.1 --- a/src/Pure/drule.ML	Mon Jul 27 16:35:12 2015 +0200
    56.2 +++ b/src/Pure/drule.ML	Mon Jul 27 17:44:55 2015 +0200
    56.3 @@ -24,7 +24,6 @@
    56.4      thm -> thm
    56.5    val infer_instantiate_types: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm
    56.6    val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
    56.7 -  val instantiate': ctyp option list -> cterm option list -> thm -> thm
    56.8    val infer_instantiate': Proof.context -> cterm option list -> thm -> thm
    56.9    val zero_var_indexes_list: thm list -> thm list
   56.10    val zero_var_indexes: thm -> thm
   56.11 @@ -798,26 +797,6 @@
   56.12            AList.lookup (op =) vars xi |> Option.map (fn T => ((xi, T), cu)));
   56.13        in infer_instantiate_types ctxt args' th end;
   56.14  
   56.15 -
   56.16 -(* instantiate by left-to-right occurrence of variables *)
   56.17 -
   56.18 -fun instantiate' cTs cts thm =
   56.19 -  let
   56.20 -    fun err msg =
   56.21 -      raise TYPE ("instantiate': " ^ msg,
   56.22 -        map_filter (Option.map Thm.typ_of) cTs,
   56.23 -        map_filter (Option.map Thm.term_of) cts);
   56.24 -
   56.25 -    fun zip_vars xs ys =
   56.26 -      zip_options xs ys handle ListPair.UnequalLengths =>
   56.27 -        err "more instantiations than variables in thm";
   56.28 -
   56.29 -    val thm' =
   56.30 -      Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
   56.31 -    val thm'' =
   56.32 -      Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
   56.33 -  in thm'' end;
   56.34 -
   56.35  fun infer_instantiate' ctxt args th =
   56.36    let
   56.37      val vars = rev (Term.add_vars (Thm.full_prop_of th) []);
    57.1 --- a/src/Pure/more_thm.ML	Mon Jul 27 16:35:12 2015 +0200
    57.2 +++ b/src/Pure/more_thm.ML	Mon Jul 27 17:44:55 2015 +0200
    57.3 @@ -60,6 +60,7 @@
    57.4    val elim_implies: thm -> thm -> thm
    57.5    val forall_elim_var: int -> thm -> thm
    57.6    val forall_elim_vars: int -> thm -> thm
    57.7 +  val instantiate': ctyp option list -> cterm option list -> thm -> thm
    57.8    val global_certify_inst: theory ->
    57.9      ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
   57.10      ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   57.11 @@ -354,6 +355,26 @@
   57.12  end;
   57.13  
   57.14  
   57.15 +(* instantiate by left-to-right occurrence of variables *)
   57.16 +
   57.17 +fun instantiate' cTs cts thm =
   57.18 +  let
   57.19 +    fun err msg =
   57.20 +      raise TYPE ("instantiate': " ^ msg,
   57.21 +        map_filter (Option.map Thm.typ_of) cTs,
   57.22 +        map_filter (Option.map Thm.term_of) cts);
   57.23 +
   57.24 +    fun zip_vars xs ys =
   57.25 +      zip_options xs ys handle ListPair.UnequalLengths =>
   57.26 +        err "more instantiations than variables in thm";
   57.27 +
   57.28 +    val thm' =
   57.29 +      Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
   57.30 +    val thm'' =
   57.31 +      Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
   57.32 +  in thm'' end;
   57.33 +
   57.34 +
   57.35  (* certify_instantiate *)
   57.36  
   57.37  fun global_certify_inst thy (instT, inst) =
    58.1 --- a/src/Tools/atomize_elim.ML	Mon Jul 27 16:35:12 2015 +0200
    58.2 +++ b/src/Tools/atomize_elim.ML	Mon Jul 27 17:44:55 2015 +0200
    58.3 @@ -117,7 +117,7 @@
    58.4            if is_Bound thesis then all_tac
    58.5            else let
    58.6                val cthesis = Thm.global_cterm_of thy thesis
    58.7 -              val rule = instantiate' [SOME (Thm.ctyp_of_cterm cthesis)] [NONE, SOME cthesis]
    58.8 +              val rule = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cthesis)] [NONE, SOME cthesis]
    58.9                           @{thm meta_spec}
   58.10              in
   58.11                compose_tac ctxt (false, rule, 1) i