merged
authorwenzelm
Mon Jul 27 22:08:46 2015 +0200 (2015-07-27)
changeset 60803e11f47dd0786
parent 60800 7d04351c795a
parent 60802 067658d63c5d
child 60804 080a979a985b
child 60805 4cc49ead6e75
merged
     1.1 --- a/NEWS	Mon Jul 27 16:52:57 2015 +0100
     1.2 +++ b/NEWS	Mon Jul 27 22:08:46 2015 +0200
     1.3 @@ -246,6 +246,18 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Instantiation rules have been re-organized as follows:
     1.8 +
     1.9 +  Thm.instantiate  (*low-level instantiation with named arguments*)
    1.10 +  Thm.instantiate' (*version with positional arguments*)
    1.11 +
    1.12 +  Drule.infer_instantiate  (*instantiation with type inference*)
    1.13 +  Drule.infer_instantiate'  (*version with positional arguments*)
    1.14 +
    1.15 +The LHS only requires variable specifications, instead of full terms.
    1.16 +Old cterm_instantiate is superseded by infer_instantiate.
    1.17 +INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.
    1.18 +
    1.19  * Old tactic shorthands atac, rtac, etac, dtac, ftac have been
    1.20  discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
    1.21  instead (with proper context).
     2.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Jul 27 16:52:57 2015 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Jul 27 22:08:46 2015 +0200
     2.3 @@ -906,7 +906,7 @@
     2.4    let val (a, b) = Rat.quotient_of_rat x
     2.5    in if b = 1 then Numeral.mk_cnumber cT a
     2.6      else Thm.apply
     2.7 -         (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
     2.8 +         (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"})
     2.9                       (Numeral.mk_cnumber cT a))
    2.10           (Numeral.mk_cnumber cT b)
    2.11   end
    2.12 @@ -939,7 +939,7 @@
    2.13                    (if neg then Thm.apply (Thm.apply clt c) cz
    2.14                      else Thm.apply (Thm.apply clt cz) c))
    2.15          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    2.16 -        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
    2.17 +        val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
    2.18               (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
    2.19          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.20                     (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.21 @@ -947,7 +947,7 @@
    2.22      | ("x+t",[t]) =>
    2.23         let
    2.24          val T = Thm.ctyp_of_cterm x
    2.25 -        val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
    2.26 +        val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
    2.27          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.28                (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.29         in  rth end
    2.30 @@ -962,7 +962,7 @@
    2.31                    (if neg then Thm.apply (Thm.apply clt c) cz
    2.32                      else Thm.apply (Thm.apply clt cz) c))
    2.33          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    2.34 -        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
    2.35 +        val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
    2.36               (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
    2.37          val rth = th
    2.38        in rth end
    2.39 @@ -975,7 +975,7 @@
    2.40         let
    2.41          val T = Thm.ctyp_of_cterm x
    2.42          val cr = dest_frac c
    2.43 -        val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
    2.44 +        val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"}
    2.45          val cz = Thm.dest_arg ct
    2.46          val neg = cr </ Rat.zero
    2.47          val cthp = Simplifier.rewrite ctxt
    2.48 @@ -983,7 +983,7 @@
    2.49                    (if neg then Thm.apply (Thm.apply clt c) cz
    2.50                      else Thm.apply (Thm.apply clt cz) c))
    2.51          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    2.52 -        val th = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
    2.53 +        val th = Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [c,x,t])
    2.54               (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
    2.55          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.56                     (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.57 @@ -991,7 +991,7 @@
    2.58      | ("x+t",[t]) =>
    2.59         let
    2.60          val T = Thm.ctyp_of_cterm x
    2.61 -        val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
    2.62 +        val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
    2.63          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.64                (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.65         in  rth end
    2.66 @@ -999,7 +999,7 @@
    2.67         let
    2.68          val T = Thm.ctyp_of_cterm x
    2.69          val cr = dest_frac c
    2.70 -        val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
    2.71 +        val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"}
    2.72          val cz = Thm.dest_arg ct
    2.73          val neg = cr </ Rat.zero
    2.74          val cthp = Simplifier.rewrite ctxt
    2.75 @@ -1007,7 +1007,7 @@
    2.76                    (if neg then Thm.apply (Thm.apply clt c) cz
    2.77                      else Thm.apply (Thm.apply clt cz) c))
    2.78          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    2.79 -        val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
    2.80 +        val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
    2.81               (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
    2.82          val rth = th
    2.83        in rth end
    2.84 @@ -1026,14 +1026,14 @@
    2.85               (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
    2.86          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    2.87          val th = Thm.implies_elim
    2.88 -                 (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
    2.89 +                 (Thm.instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
    2.90          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.91                     (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
    2.92        in rth end
    2.93      | ("x+t",[t]) =>
    2.94         let
    2.95          val T = Thm.ctyp_of_cterm x
    2.96 -        val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
    2.97 +        val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
    2.98          val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
    2.99                (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
   2.100         in  rth end
   2.101 @@ -1048,7 +1048,7 @@
   2.102               (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
   2.103          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
   2.104          val rth = Thm.implies_elim
   2.105 -                 (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
   2.106 +                 (Thm.instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
   2.107        in rth end
   2.108      | _ => Thm.reflexive ct);
   2.109  
   2.110 @@ -1062,7 +1062,7 @@
   2.111    Const(@{const_name Orderings.less},_)$a$b =>
   2.112     let val (ca,cb) = Thm.dest_binop ct
   2.113         val T = Thm.ctyp_of_cterm ca
   2.114 -       val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
   2.115 +       val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
   2.116         val nth = Conv.fconv_rule
   2.117           (Conv.arg_conv (Conv.arg1_conv
   2.118                (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
   2.119 @@ -1071,7 +1071,7 @@
   2.120  | Const(@{const_name Orderings.less_eq},_)$a$b =>
   2.121     let val (ca,cb) = Thm.dest_binop ct
   2.122         val T = Thm.ctyp_of_cterm ca
   2.123 -       val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
   2.124 +       val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
   2.125         val nth = Conv.fconv_rule
   2.126           (Conv.arg_conv (Conv.arg1_conv
   2.127                (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
   2.128 @@ -1081,7 +1081,7 @@
   2.129  | Const(@{const_name HOL.eq},_)$a$b =>
   2.130     let val (ca,cb) = Thm.dest_binop ct
   2.131         val T = Thm.ctyp_of_cterm ca
   2.132 -       val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
   2.133 +       val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
   2.134         val nth = Conv.fconv_rule
   2.135           (Conv.arg_conv (Conv.arg1_conv
   2.136                (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
     3.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Mon Jul 27 16:52:57 2015 +0100
     3.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Mon Jul 27 22:08:46 2015 +0200
     3.3 @@ -96,7 +96,7 @@
     3.4      val cring_ctxt = ctxt addsimps cring_simps;  (*FIXME really the full simpset!?*)
     3.5      val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g);
     3.6      val norm_eq_th = (* may collapse to True *)
     3.7 -      simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
     3.8 +      simplify cring_ctxt (Thm.instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
     3.9    in
    3.10      cut_tac norm_eq_th i
    3.11      THEN (simp_tac cring_ctxt i)
     4.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Mon Jul 27 16:52:57 2015 +0100
     4.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Mon Jul 27 22:08:46 2015 +0200
     4.3 @@ -87,23 +87,23 @@
     4.4     val q = Thm.rhs_of nth
     4.5     val qx = Thm.rhs_of nthx
     4.6     val enth = Drule.arg_cong_rule ce nthx
     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 (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
    4.11 +      Thm.implies_elim (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
    4.12                                         (Thm.cprop_of th), SOME x] th1) th
    4.13     val fU = fold ins u th0
    4.14     val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU)
    4.15     local
    4.16 -     val insI1 = instantiate' [SOME cT] [] @{thm "insertI1"}
    4.17 -     val insI2 = instantiate' [SOME cT] [] @{thm "insertI2"}
    4.18 +     val insI1 = Thm.instantiate' [SOME cT] [] @{thm "insertI1"}
    4.19 +     val insI2 = Thm.instantiate' [SOME cT] [] @{thm "insertI2"}
    4.20     in
    4.21      fun provein x S =
    4.22       case Thm.term_of S of
    4.23          Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S])
    4.24        | Const(@{const_name insert}, _) $ y $_ =>
    4.25           let val (cy,S') = Thm.dest_binop S
    4.26 -         in if Thm.term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
    4.27 -         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
    4.28 +         in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1
    4.29 +         else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2)
    4.30                             (provein x S')
    4.31           end
    4.32     end
    4.33 @@ -141,11 +141,11 @@
    4.34                        else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
    4.35                        else raise Fail "decomp_mpinf: Impossible case!!") fm
    4.36               val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
    4.37 -               if c = Nox then map (instantiate' [] [SOME fm])
    4.38 +               if c = Nox then map (Thm.instantiate' [] [SOME fm])
    4.39                                      [minf_P, pinf_P, nmi_P, npi_P, ld_P]
    4.40                 else
    4.41                  let val [mi_th,pi_th,nmi_th,npi_th,ld_th] =
    4.42 -                 map (instantiate' [] [SOME t])
    4.43 +                 map (Thm.instantiate' [] [SOME t])
    4.44                   (case c of Lt => [minf_lt, pinf_lt, nmi_lt, npi_lt, ld_lt]
    4.45                            | Le => [minf_le, pinf_le, nmi_le, npi_le, ld_le]
    4.46                            | Gt => [minf_gt, pinf_gt, nmi_gt, npi_gt, ld_gt]
    4.47 @@ -160,7 +160,7 @@
    4.48     val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q
    4.49     val qe_th = Drule.implies_elim_list
    4.50                    ((fconv_rule (Thm.beta_conversion true))
    4.51 -                   (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
    4.52 +                   (Thm.instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
    4.53                          qe))
    4.54                    [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
    4.55      val bex_conv =
     5.1 --- a/src/HOL/Decision_Procs/langford.ML	Mon Jul 27 16:52:57 2015 +0100
     5.2 +++ b/src/HOL/Decision_Procs/langford.ML	Mon Jul 27 22:08:46 2015 +0200
     5.3 @@ -21,10 +21,10 @@
     5.4  
     5.5  fun prove_finite cT u =
     5.6    let
     5.7 -    val [th0, th1] = map (instantiate' [SOME cT] []) @{thms finite.intros}
     5.8 +    val [th0, th1] = map (Thm.instantiate' [SOME cT] []) @{thms finite.intros}
     5.9      fun ins x th =
    5.10        Thm.implies_elim
    5.11 -        (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
    5.12 +        (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
    5.13    in fold ins u th0 end;
    5.14  
    5.15  fun simp_rule ctxt =
    5.16 @@ -39,7 +39,7 @@
    5.17          val p = Thm.dest_arg ep
    5.18          val ths =
    5.19            simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
    5.20 -            (instantiate' [] [SOME p] stupid)
    5.21 +            (Thm.instantiate' [] [SOME p] stupid)
    5.22          val (L, U) =
    5.23            let val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
    5.24            in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end
    5.25 @@ -47,7 +47,7 @@
    5.26            let
    5.27              val (a, A) = Thm.dest_comb S |>> Thm.dest_arg
    5.28              val cT = Thm.ctyp_of_cterm a
    5.29 -            val ne = instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
    5.30 +            val ne = Thm.instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
    5.31              val f = prove_finite cT (dest_set S)
    5.32           in (ne, f) end
    5.33  
    5.34 @@ -114,7 +114,7 @@
    5.35      val rr = Thm.dest_arg r
    5.36      val thl  = prove_conj tabl (conjuncts rr) |> Drule.implies_intr_hyps
    5.37      val thr  = prove_conj tabr (conjuncts ll) |> Drule.implies_intr_hyps
    5.38 -    val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
    5.39 +    val eqI = Thm.instantiate' [] [SOME ll, SOME rr] @{thm iffI}
    5.40    in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
    5.41  
    5.42  fun contains x ct =
    5.43 @@ -230,7 +230,7 @@
    5.44  
    5.45  fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
    5.46    let
    5.47 -    fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
    5.48 +    fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"}
    5.49      fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
    5.50      val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
    5.51      val p' = fold_rev gen ts p
     6.1 --- a/src/HOL/HOLCF/Cfun.thy	Mon Jul 27 16:52:57 2015 +0100
     6.2 +++ b/src/HOL/HOLCF/Cfun.thy	Mon Jul 27 22:08:46 2015 +0200
     6.3 @@ -145,7 +145,7 @@
     6.4        val dest = Thm.dest_comb;
     6.5        val f = (snd o dest o snd o dest) ct;
     6.6        val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
     6.7 -      val tr = instantiate' [SOME T, SOME U] [SOME f]
     6.8 +      val tr = Thm.instantiate' [SOME T, SOME U] [SOME f]
     6.9            (mk_meta_eq @{thm Abs_cfun_inverse2});
    6.10        val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
    6.11        val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
     7.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Mon Jul 27 16:52:57 2015 +0100
     7.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Mon Jul 27 22:08:46 2015 +0200
     7.3 @@ -213,7 +213,7 @@
     7.4              val (n2, t2) = cons2typ n1 cons
     7.5            in (n2, mk_ssumT (t1, t2)) end
     7.6        val ct = Thm.global_ctyp_of thy (snd (cons2typ 1 spec'))
     7.7 -      val thm1 = instantiate' [SOME ct] [] @{thm exh_start}
     7.8 +      val thm1 = Thm.instantiate' [SOME ct] [] @{thm exh_start}
     7.9        val thm2 = rewrite_rule (Proof_Context.init_global thy)
    7.10          (map mk_meta_eq @{thms ex_bottom_iffs}) thm1
    7.11        val thm3 = rewrite_rule (Proof_Context.init_global thy)
     8.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Jul 27 16:52:57 2015 +0100
     8.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Mon Jul 27 22:08:46 2015 +0200
     8.3 @@ -121,7 +121,7 @@
     8.4  local
     8.5    fun solve_cont ctxt t =
     8.6      let
     8.7 -      val tr = instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
     8.8 +      val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
     8.9      in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end
    8.10  in
    8.11    fun cont_proc thy =
     9.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Mon Jul 27 16:52:57 2015 +0100
     9.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon Jul 27 22:08:46 2015 +0200
     9.3 @@ -153,7 +153,7 @@
     9.4      val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT)
     9.5      val predicate = lambda_tuple lhss (list_comb (P, lhss))
     9.6      val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
     9.7 -      |> Drule.instantiate' [] [SOME (Thm.global_cterm_of thy predicate)]
     9.8 +      |> Thm.instantiate' [] [SOME (Thm.global_cterm_of thy predicate)]
     9.9        |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict}
    9.10      val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
    9.11        |> Local_Defs.unfold lthy @{thms split_conv}
    10.1 --- a/src/HOL/Import/import_rule.ML	Mon Jul 27 16:52:57 2015 +0100
    10.2 +++ b/src/HOL/Import/import_rule.ML	Mon Jul 27 22:08:46 2015 +0200
    10.3 @@ -55,7 +55,7 @@
    10.4    let
    10.5      val (tml, tmr) = Thm.dest_binop (strip_imp_concl (Thm.cprop_of th))
    10.6      val cty = Thm.ctyp_of_cterm tml
    10.7 -    val i = Drule.instantiate' [SOME cty] [SOME tml, SOME tmr]
    10.8 +    val i = Thm.instantiate' [SOME cty] [SOME tml, SOME tmr]
    10.9        @{thm meta_eq_to_obj_eq}
   10.10    in
   10.11      Thm.implies_elim i th
   10.12 @@ -66,7 +66,7 @@
   10.13  fun eq_mp th1 th2 =
   10.14    let
   10.15      val (tm1l, tm1r) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1)))
   10.16 -    val i1 = Drule.instantiate' [] [SOME tm1l, SOME tm1r] @{thm iffD1}
   10.17 +    val i1 = Thm.instantiate' [] [SOME tm1l, SOME tm1r] @{thm iffD1}
   10.18      val i2 = meta_mp i1 th1
   10.19    in
   10.20      meta_mp i2 th2
   10.21 @@ -79,7 +79,7 @@
   10.22      val (cf, cg) = Thm.dest_binop t1c
   10.23      val (cx, cy) = Thm.dest_binop t2c
   10.24      val [fd, fr] = Thm.dest_ctyp (Thm.ctyp_of_cterm cf)
   10.25 -    val i1 = Drule.instantiate' [SOME fd, SOME fr]
   10.26 +    val i1 = Thm.instantiate' [SOME fd, SOME fr]
   10.27        [SOME cf, SOME cg, SOME cx, SOME cy] @{thm cong}
   10.28      val i2 = meta_mp i1 th1
   10.29    in
   10.30 @@ -93,7 +93,7 @@
   10.31      val (r, s) = Thm.dest_binop t1c
   10.32      val (_, t) = Thm.dest_binop t2c
   10.33      val ty = Thm.ctyp_of_cterm r
   10.34 -    val i1 = Drule.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
   10.35 +    val i1 = Thm.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
   10.36      val i2 = meta_mp i1 th1
   10.37    in
   10.38      meta_mp i2 th2
   10.39 @@ -107,7 +107,7 @@
   10.40      val th2a = implies_elim_all th2
   10.41      val th1b = Thm.implies_intr th2c th1a
   10.42      val th2b = Thm.implies_intr th1c th2a
   10.43 -    val i = Drule.instantiate' []
   10.44 +    val i = Thm.instantiate' []
   10.45        [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
   10.46      val i1 = Thm.implies_elim i (Thm.assume (Thm.cprop_of th2b))
   10.47      val i2 = Thm.implies_elim i1 th1b
   10.48 @@ -120,7 +120,7 @@
   10.49  fun conj1 th =
   10.50    let
   10.51      val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
   10.52 -    val i = Drule.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct1}
   10.53 +    val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct1}
   10.54    in
   10.55      meta_mp i th
   10.56    end
   10.57 @@ -128,7 +128,7 @@
   10.58  fun conj2 th =
   10.59    let
   10.60      val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
   10.61 -    val i = Drule.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct2}
   10.62 +    val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct2}
   10.63    in
   10.64      meta_mp i th
   10.65    end
   10.66 @@ -137,7 +137,7 @@
   10.67    let
   10.68      val cty = Thm.ctyp_of_cterm ctm
   10.69    in
   10.70 -    Drule.instantiate' [SOME cty] [SOME ctm] @{thm refl}
   10.71 +    Thm.instantiate' [SOME cty] [SOME ctm] @{thm refl}
   10.72    end
   10.73  
   10.74  fun abs cv th =
   10.75 @@ -151,7 +151,7 @@
   10.76      val th2 = trans (trans bl th1) br
   10.77      val th3 = implies_elim_all th2
   10.78      val th4 = Thm.forall_intr cv th3
   10.79 -    val i = Drule.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)]
   10.80 +    val i = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)]
   10.81        [SOME ll, SOME lr] @{thm ext2}
   10.82    in
   10.83      meta_mp i th4
   10.84 @@ -202,7 +202,7 @@
   10.85      val P = Thm.dest_arg cn
   10.86      val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
   10.87    in
   10.88 -    Drule.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
   10.89 +    Thm.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
   10.90        SOME (Thm.global_cterm_of thy (Free ("a", Thm.typ_of nty))),
   10.91        SOME (Thm.global_cterm_of thy (Free ("r", Thm.typ_of oty)))] @{thm typedef_hol2hollight}
   10.92    end
   10.93 @@ -210,7 +210,7 @@
   10.94  fun tydef' tycname abs_name rep_name cP ct td_th thy =
   10.95    let
   10.96      val ctT = Thm.ctyp_of_cterm ct
   10.97 -    val nonempty = Drule.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
   10.98 +    val nonempty = Thm.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
   10.99      val th2 = meta_mp nonempty td_th
  10.100      val c =
  10.101        case Thm.concl_of th2 of
  10.102 @@ -228,7 +228,7 @@
  10.103      val rept = Thm.dest_arg th_s
  10.104      val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
  10.105      val typedef_th =
  10.106 -       Drule.instantiate'
  10.107 +       Thm.instantiate'
  10.108            [SOME nty, SOME oty]
  10.109            [SOME rept, SOME abst, SOME cP, SOME (Thm.global_cterm_of thy' (Free ("a", aty))),
  10.110               SOME (Thm.global_cterm_of thy' (Free ("r", Thm.typ_of ctT)))]
    11.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Mon Jul 27 16:52:57 2015 +0100
    11.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Mon Jul 27 22:08:46 2015 +0200
    11.3 @@ -77,7 +77,7 @@
    11.4          val thm' =
    11.5            Thm.implies_elim
    11.6             (Conv.fconv_rule (Thm.beta_conversion true)
    11.7 -             (Drule.instantiate'
    11.8 +             (Thm.instantiate'
    11.9                 [SOME (Thm.ctyp_of_cterm ct)] [SOME (Thm.lambda cv ct),
   11.10                   SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv']
   11.11                 Suc_if_eq)) (Thm.forall_intr cv' thm)
    12.1 --- a/src/HOL/Library/Countable.thy	Mon Jul 27 16:52:57 2015 +0100
    12.2 +++ b/src/HOL/Library/Countable.thy	Mon Jul 27 22:08:46 2015 +0200
    12.3 @@ -182,7 +182,7 @@
    12.4          val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
    12.5          val insts = vars |> map (fn (_, T) => try (Thm.cterm_of ctxt)
    12.6            (Const (@{const_name Countable.finite_item}, T)))
    12.7 -        val induct_thm' = Drule.instantiate' [] insts induct_thm
    12.8 +        val induct_thm' = Thm.instantiate' [] insts induct_thm
    12.9          val rules = @{thms finite_item.intros}
   12.10        in
   12.11          SOLVED' (fn i => EVERY
    13.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon Jul 27 16:52:57 2015 +0100
    13.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon Jul 27 22:08:46 2015 +0200
    13.3 @@ -1047,7 +1047,7 @@
    13.4            ctxt addsimps @{thms field_simps}
    13.5            addsimps [@{thm nonzero_power_divide}, @{thm power_divide}]
    13.6          val th =
    13.7 -          instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
    13.8 +          Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
    13.9              (if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
   13.10               else @{lemma "(d=0 --> P) & (d ~= (0::real) --> P) ==> P" by blast})
   13.11        in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
    14.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Jul 27 16:52:57 2015 +0100
    14.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Jul 27 22:08:46 2015 +0200
    14.3 @@ -317,7 +317,7 @@
    14.4    | _ => raise CTERM ("find_cterm",[t]);
    14.5  
    14.6      (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
    14.7 -fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
    14.8 +fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
    14.9  fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
   14.10  
   14.11  fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
   14.12 @@ -396,9 +396,9 @@
   14.13      fun add_rule th th' = fconv_rule (arg_conv (oprconv poly_add_conv))
   14.14           (match_mp_rule pth_add [th, th'])
   14.15      fun emul_rule ct th = fconv_rule (arg_conv (oprconv poly_mul_conv))
   14.16 -       (instantiate' [] [SOME ct] (th RS pth_emul))
   14.17 +       (Thm.instantiate' [] [SOME ct] (th RS pth_emul))
   14.18      fun square_rule t = fconv_rule (arg_conv (oprconv poly_conv))
   14.19 -       (instantiate' [] [SOME t] pth_square)
   14.20 +       (Thm.instantiate' [] [SOME t] pth_square)
   14.21  
   14.22      fun hol_of_positivstellensatz(eqs,les,lts) proof =
   14.23        let
   14.24 @@ -444,7 +444,7 @@
   14.25            if c aconvc (concl th2) then ()
   14.26            else error "disj_cases : conclusions not alpha convertible"
   14.27        in Thm.implies_elim (Thm.implies_elim
   14.28 -          (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
   14.29 +          (Thm.implies_elim (Thm.instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
   14.30            (Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
   14.31          (Thm.implies_intr (Thm.apply @{cterm Trueprop} q) th2)
   14.32        end
   14.33 @@ -518,9 +518,9 @@
   14.34          (instantiate_cterm' [SOME (Thm.ctyp_of_cterm x)] [] @{cpat "All :: (?'a => bool) => _" })
   14.35          (Thm.abstract_rule (name_of x) x th)
   14.36  
   14.37 -    val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   14.38 +    val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
   14.39  
   14.40 -    fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   14.41 +    fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
   14.42      fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
   14.43  
   14.44      fun choose v th th' =
   14.45 @@ -530,7 +530,7 @@
   14.46            val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
   14.47            val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
   14.48            val th0 = fconv_rule (Thm.beta_conversion true)
   14.49 -            (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   14.50 +            (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   14.51            val pv = (Thm.rhs_of o Thm.beta_conversion true)
   14.52              (Thm.apply @{cterm Trueprop} (Thm.apply p v))
   14.53            val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
   14.54 @@ -579,7 +579,7 @@
   14.55                  (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
   14.56            in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
   14.57            end
   14.58 -      in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
   14.59 +      in (Thm.implies_elim (Thm.instantiate' [] [SOME ct] pth_final) th, certificates)
   14.60        end
   14.61    in f
   14.62    end;
   14.63 @@ -710,7 +710,7 @@
   14.64                  (eq_pols @ le_pols @ lt_pols) [])
   14.65      val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
   14.66      val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
   14.67 -    val le' = le @ map (fn a => instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens
   14.68 +    val le' = le @ map (fn a => Thm.instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens
   14.69    in ((translator (eq,le',lt) proof), Trivial)
   14.70    end
   14.71  end;
   14.72 @@ -725,9 +725,9 @@
   14.73  
   14.74    val absmaxmin_elim_conv2 =
   14.75      let
   14.76 -      val pth_abs = instantiate' [SOME @{ctyp real}] [] abs_split'
   14.77 -      val pth_max = instantiate' [SOME @{ctyp real}] [] max_split
   14.78 -      val pth_min = instantiate' [SOME @{ctyp real}] [] min_split
   14.79 +      val pth_abs = Thm.instantiate' [SOME @{ctyp real}] [] abs_split'
   14.80 +      val pth_max = Thm.instantiate' [SOME @{ctyp real}] [] max_split
   14.81 +      val pth_min = Thm.instantiate' [SOME @{ctyp real}] [] min_split
   14.82        val abs_tm = @{cterm "abs :: real => _"}
   14.83        val p_v = (("P", 0), @{typ "real \<Rightarrow> bool"})
   14.84        val x_v = (("x", 0), @{typ real})
    15.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Mon Jul 27 16:52:57 2015 +0100
    15.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Mon Jul 27 22:08:46 2015 +0200
    15.3 @@ -154,7 +154,7 @@
    15.4          (Numeral.mk_cnumber @{ctyp "real"} b)
    15.5  end;
    15.6  
    15.7 -fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
    15.8 +fun norm_cmul_rule c th = Thm.instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
    15.9  
   15.10  fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm};
   15.11  
   15.12 @@ -342,7 +342,7 @@
   15.13    val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) []
   15.14    val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
   15.15    val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
   15.16 -  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
   15.17 +  fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
   15.18    fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   15.19    fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   15.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
    16.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Jul 27 16:52:57 2015 +0100
    16.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Jul 27 22:08:46 2015 +0200
    16.3 @@ -110,7 +110,7 @@
    16.4              val dj_cp' = [cp, dj] MRS dj_cp;
    16.5              val cert = SOME o Thm.cterm_of ctxt
    16.6            in
    16.7 -            SOME (mk_meta_eq (Drule.instantiate' [SOME (Thm.ctyp_of ctxt S)]
    16.8 +            SOME (mk_meta_eq (Thm.instantiate' [SOME (Thm.ctyp_of ctxt S)]
    16.9                [cert t, cert r, cert s] dj_cp'))
   16.10            end
   16.11          else NONE
   16.12 @@ -1282,7 +1282,7 @@
   16.13              _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ _)) $ _ => U = T
   16.14            | _ => false)) perm_fresh_fresh
   16.15        in
   16.16 -        Drule.instantiate' []
   16.17 +        Thm.instantiate' []
   16.18            [SOME (Thm.global_cterm_of thy a), NONE, SOME (Thm.global_cterm_of thy b)] th
   16.19        end;
   16.20  
    17.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon Jul 27 16:52:57 2015 +0100
    17.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Jul 27 22:08:46 2015 +0200
    17.3 @@ -203,7 +203,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 @@ -488,7 +488,7 @@
   17.13                           let
   17.14                             val (cf, ct) =
   17.15                               Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th));
   17.16 -                           val arg_cong' = Drule.instantiate'
   17.17 +                           val arg_cong' = Thm.instantiate'
   17.18                               [SOME (Thm.ctyp_of_cterm ct)]
   17.19                               [NONE, SOME ct, SOME cf] (arg_cong RS iffD2);
   17.20                             val inst = Thm.first_order_match (ct,
    18.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Mon Jul 27 16:52:57 2015 +0100
    18.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Jul 27 22:08:46 2015 +0200
    18.3 @@ -227,7 +227,7 @@
    18.4      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    18.5      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    18.6  
    18.7 -    val inductive_forall_def' = Drule.instantiate'
    18.8 +    val inductive_forall_def' = Thm.instantiate'
    18.9        [SOME (Thm.global_ctyp_of thy fsT)] [] inductive_forall_def;
   18.10  
   18.11      fun lift_pred' t (Free (s, T)) ts =
   18.12 @@ -316,7 +316,7 @@
   18.13          val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
   18.14          val fs_atom = Global_Theory.get_thm thy
   18.15            ("fs_" ^ Long_Name.base_name atom ^ "1");
   18.16 -        val avoid_th = Drule.instantiate'
   18.17 +        val avoid_th = Thm.instantiate'
   18.18            [SOME (Thm.global_ctyp_of thy (fastype_of p))] [SOME (Thm.global_cterm_of thy p)]
   18.19            ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
   18.20          val (([(_, cx)], th1 :: th2 :: ths), ctxt') = Obtain.result
    19.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Mon Jul 27 16:52:57 2015 +0100
    19.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Jul 27 22:08:46 2015 +0200
    19.3 @@ -197,13 +197,13 @@
    19.4      in
    19.5        if pi1 <> pi2 then  (* only apply the composition rule in this case *)
    19.6          if T = U then    
    19.7 -          SOME (Drule.instantiate'
    19.8 +          SOME (Thm.instantiate'
    19.9              [SOME (Thm.global_ctyp_of thy (fastype_of t))]
   19.10              [SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
   19.11              (mk_meta_eq ([Global_Theory.get_thm thy ("pt_"^tname'^"_inst"),
   19.12               Global_Theory.get_thm thy ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
   19.13          else
   19.14 -          SOME (Drule.instantiate'
   19.15 +          SOME (Thm.instantiate'
   19.16              [SOME (Thm.global_ctyp_of thy (fastype_of t))]
   19.17              [SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
   19.18              (mk_meta_eq (Global_Theory.get_thm thy ("cp_"^tname'^"_"^uname'^"_inst") RS 
    20.1 --- a/src/HOL/Probability/measurable.ML	Mon Jul 27 16:52:57 2015 +0100
    20.2 +++ b/src/HOL/Probability/measurable.ML	Mon Jul 27 22:08:46 2015 +0200
    20.3 @@ -252,7 +252,7 @@
    20.4            val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
    20.5            fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
    20.6            fun inst (ts, Ts) =
    20.7 -            Drule.instantiate' (cert Thm.global_ctyp_of Ts) (cert Thm.global_cterm_of ts)
    20.8 +            Thm.instantiate' (cert Thm.global_ctyp_of Ts) (cert Thm.global_cterm_of ts)
    20.9                @{thm measurable_compose_countable}
   20.10          in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end
   20.11          handle TERM _ => no_tac) 1)
    21.1 --- a/src/HOL/String.thy	Mon Jul 27 16:52:57 2015 +0100
    21.2 +++ b/src/HOL/String.thy	Mon Jul 27 22:08:46 2015 +0200
    21.3 @@ -253,7 +253,7 @@
    21.4      put_simpset HOL_ss @{context}
    21.5        addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
    21.6    fun mk_code_eqn x y =
    21.7 -    Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
    21.8 +    Thm.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
    21.9      |> simplify simpset;
   21.10    val code_eqns = map_product mk_code_eqn nibbles nibbles;
   21.11  in
    22.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Jul 27 16:52:57 2015 +0100
    22.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Jul 27 22:08:46 2015 +0200
    22.3 @@ -1251,7 +1251,7 @@
    22.4                      map Bound (live - 1 downto 0)) $ Bound live));
    22.5                  val cts = [NONE, SOME (Thm.cterm_of lthy tinst)];
    22.6                in
    22.7 -                Drule.instantiate' cTs cts @{thm surj_imp_ordLeq}
    22.8 +                Thm.instantiate' cTs cts @{thm surj_imp_ordLeq}
    22.9                end);
   22.10              val bd = mk_cexp
   22.11                (if live = 0 then ctwo
    23.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jul 27 16:52:57 2015 +0100
    23.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jul 27 22:08:46 2015 +0200
    23.3 @@ -1838,7 +1838,7 @@
    23.4  
    23.5          val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
    23.6  
    23.7 -        fun mk_case_split' cp = Drule.instantiate' [] [SOME (Thm.cterm_of lthy cp)] @{thm case_split};
    23.8 +        fun mk_case_split' cp = Thm.instantiate' [] [SOME (Thm.cterm_of lthy cp)] @{thm case_split};
    23.9  
   23.10          val case_splitss' = map (map mk_case_split') cpss;
   23.11  
   23.12 @@ -1864,7 +1864,7 @@
   23.13        let
   23.14          val (domT, ranT) = dest_funT (fastype_of sel);
   23.15          val arg_cong' =
   23.16 -          Drule.instantiate' (map (SOME o Thm.ctyp_of lthy) [domT, ranT])
   23.17 +          Thm.instantiate' (map (SOME o Thm.ctyp_of lthy) [domT, ranT])
   23.18              [NONE, NONE, SOME (Thm.cterm_of lthy sel)] arg_cong
   23.19            |> Thm.varifyT_global;
   23.20          val sel_thm' = sel_thm RSN (2, trans);
    24.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jul 27 16:52:57 2015 +0100
    24.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jul 27 22:08:46 2015 +0200
    24.3 @@ -142,7 +142,7 @@
    24.4  fun mk_ctor_iff_dtor_tac ctxt cTs cctor cdtor ctor_dtor dtor_ctor =
    24.5    HEADGOAL (rtac ctxt iffI THEN'
    24.6      EVERY' (@{map 3} (fn cTs => fn cx => fn th =>
    24.7 -      dtac ctxt (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
    24.8 +      dtac ctxt (Thm.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
    24.9        SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN'
   24.10        assume_tac ctxt) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor]));
   24.11  
    25.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jul 27 16:52:57 2015 +0100
    25.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jul 27 22:08:46 2015 +0200
    25.3 @@ -497,7 +497,7 @@
    25.4        val T = mk_tupleT_balanced tfrees;
    25.5      in
    25.6        @{thm asm_rl[of "ALL x. P x --> Q x" for P Q]}
    25.7 -      |> Drule.instantiate' [SOME (Thm.ctyp_of @{context} T)] []
    25.8 +      |> Thm.instantiate' [SOME (Thm.ctyp_of @{context} T)] []
    25.9        |> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]}
   25.10        |> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
   25.11        |> Thm.varifyT_global
    26.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jul 27 16:52:57 2015 +0100
    26.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jul 27 22:08:46 2015 +0200
    26.3 @@ -1975,7 +1975,7 @@
    26.4            in
    26.5              @{map 6} (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
    26.6                ((set_minimal
    26.7 -                |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y')
    26.8 +                |> Thm.instantiate' cTs (mk_induct_tinst phis jsets y y')
    26.9                  |> unfold_thms lthy incls) OF
   26.10                  (replicate n ballI @
   26.11                    maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
   26.12 @@ -2107,7 +2107,7 @@
   26.13              val cphis = @{map 9} mk_cphi
   26.14                Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
   26.15  
   26.16 -            val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
   26.17 +            val coinduct = Thm.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
   26.18  
   26.19              val goal =
   26.20                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    27.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Jul 27 16:52:57 2015 +0100
    27.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Jul 27 22:08:46 2015 +0200
    27.3 @@ -157,7 +157,7 @@
    27.4      let
    27.5        val s = Name.uu;
    27.6        val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
    27.7 -      val split' = Drule.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split;
    27.8 +      val split' = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split;
    27.9      in
   27.10        Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
   27.11      end
    28.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Jul 27 16:52:57 2015 +0100
    28.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Jul 27 22:08:46 2015 +0200
    28.3 @@ -175,7 +175,7 @@
    28.4      rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1;
    28.5  
    28.6  fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs =
    28.7 -  EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
    28.8 +  EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
    28.9      REPEAT_DETERM o rtac ctxt allI,
   28.10      CONJ_WRAP' (fn thm => EVERY'
   28.11        [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm empty_subsetI}]) rec_0s,
   28.12 @@ -195,7 +195,7 @@
   28.13      REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], assume_tac ctxt])) (1 upto n)) 1
   28.14  
   28.15  fun mk_mor_col_tac ctxt m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss =
   28.16 -  EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   28.17 +  EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   28.18      REPEAT_DETERM o rtac ctxt allI,
   28.19      CONJ_WRAP' (fn thm => EVERY' (map (rtac ctxt) [impI, thm RS trans, thm RS sym])) rec_0s,
   28.20      REPEAT_DETERM o rtac ctxt allI,
   28.21 @@ -400,7 +400,7 @@
   28.22      val n = length Lev_0s;
   28.23      val ks = n downto 1;
   28.24    in
   28.25 -    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   28.26 +    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   28.27        REPEAT_DETERM o rtac ctxt allI,
   28.28        CONJ_WRAP' (fn Lev_0 =>
   28.29          EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
   28.30 @@ -425,7 +425,7 @@
   28.31      val n = length rv_Nils;
   28.32      val ks = 1 upto n;
   28.33    in
   28.34 -    EVERY' [rtac ctxt (Drule.instantiate' cTs cts @{thm list.induct}),
   28.35 +    EVERY' [rtac ctxt (Thm.instantiate' cTs cts @{thm list.induct}),
   28.36        REPEAT_DETERM o rtac ctxt allI,
   28.37        CONJ_WRAP' (fn rv_Cons =>
   28.38          CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac ctxt exI,
   28.39 @@ -450,7 +450,7 @@
   28.40      val n = length Lev_0s;
   28.41      val ks = 1 upto n;
   28.42    in
   28.43 -    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   28.44 +    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   28.45        REPEAT_DETERM o rtac ctxt allI,
   28.46        CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
   28.47          EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
   28.48 @@ -496,7 +496,7 @@
   28.49      val n = length Lev_0s;
   28.50      val ks = 1 upto n;
   28.51    in
   28.52 -    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   28.53 +    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   28.54        REPEAT_DETERM o rtac ctxt allI,
   28.55        CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
   28.56          EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
   28.57 @@ -867,7 +867,7 @@
   28.58    let
   28.59      val n = length dtor_maps;
   28.60    in
   28.61 -    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   28.62 +    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   28.63        REPEAT_DETERM o rtac ctxt allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
   28.64        CONJ_WRAP' (K (rtac ctxt @{thm image_empty})) rec_0s,
   28.65        REPEAT_DETERM o rtac ctxt allI,
   28.66 @@ -889,7 +889,7 @@
   28.67    let
   28.68      val n = length rec_0s;
   28.69    in
   28.70 -    EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
   28.71 +    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
   28.72        REPEAT_DETERM o rtac ctxt allI,
   28.73        CONJ_WRAP' (fn rec_0 => EVERY' (map (rtac ctxt) [ordIso_ordLeq_trans,
   28.74          @{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s,
    29.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Jul 27 16:52:57 2015 +0100
    29.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Jul 27 22:08:46 2015 +0200
    29.3 @@ -1581,7 +1581,7 @@
    29.4                (@{map 4} (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
    29.5  
    29.6              val inducts = map (fn cphis =>
    29.7 -              Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
    29.8 +              Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
    29.9  
   29.10              val goals =
   29.11                @{map 3} (fn f => fn sets => fn sets' =>
   29.12 @@ -1610,7 +1610,7 @@
   29.13              val cphiss = map (map2 mk_cphi Izs) Isetss_by_range;
   29.14  
   29.15              val inducts = map (fn cphis =>
   29.16 -              Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
   29.17 +              Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
   29.18  
   29.19              val goals =
   29.20                map (fn sets =>
   29.21 @@ -1645,7 +1645,7 @@
   29.22  
   29.23              val cphis = @{map 4} mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
   29.24  
   29.25 -            val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
   29.26 +            val induct = Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
   29.27  
   29.28              val goal =
   29.29                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   29.30 @@ -1706,7 +1706,7 @@
   29.31              val cxs = map (SOME o Thm.cterm_of lthy) (splice Izs1 Izs2);
   29.32              fun mk_cphi z1 z2 goal = SOME (Thm.cterm_of lthy (Term.absfree z1 (Term.absfree z2 goal)));
   29.33              val cphis = @{map 3} mk_cphi Izs1' Izs2' goals;
   29.34 -            val induct = Drule.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
   29.35 +            val induct = Thm.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
   29.36  
   29.37              val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
   29.38            in
    30.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Jul 27 16:52:57 2015 +0100
    30.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Jul 27 22:08:46 2015 +0200
    30.3 @@ -222,7 +222,7 @@
    30.4    suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite =
    30.5    let
    30.6      val induct = worel RS
    30.7 -      Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
    30.8 +      Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
    30.9      val src = 1 upto m + 1;
   30.10      val dest = (m + 1) :: (1 upto m);
   30.11      val absorbAs_tac = if m = 0 then K (all_tac)
   30.12 @@ -268,7 +268,7 @@
   30.13  fun mk_min_algs_least_tac ctxt cT ct worel min_algs alg_sets =
   30.14    let
   30.15      val induct = worel RS
   30.16 -      Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
   30.17 +      Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
   30.18  
   30.19      val minG_tac =
   30.20        EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E},
   30.21 @@ -444,7 +444,7 @@
   30.22  fun mk_mor_fold_tac ctxt cT ct fold_defs ex_mor mor =
   30.23    (EVERY' (map (stac ctxt) fold_defs) THEN' EVERY' [rtac ctxt rev_mp, rtac ctxt ex_mor, rtac ctxt impI] THEN'
   30.24    REPEAT_DETERM_N (length fold_defs) o etac ctxt exE THEN'
   30.25 -  rtac ctxt (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1;
   30.26 +  rtac ctxt (Thm.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1;
   30.27  
   30.28  fun mk_fold_unique_mor_tac ctxt type_defs init_unique_mors Reps mor_comp mor_Abs mor_fold =
   30.29    let
   30.30 @@ -515,7 +515,7 @@
   30.31              assume_tac ctxt],
   30.32          assume_tac ctxt];
   30.33    in
   30.34 -    EVERY' [rtac ctxt rev_mp, rtac ctxt (Drule.instantiate' cTs cts ctor_induct),
   30.35 +    EVERY' [rtac ctxt rev_mp, rtac ctxt (Thm.instantiate' cTs cts ctor_induct),
   30.36        EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac ctxt impI,
   30.37        REPEAT_DETERM o eresolve_tac ctxt [conjE, allE],
   30.38        CONJ_WRAP' (K (assume_tac ctxt)) ks] 1
    31.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jul 27 16:52:57 2015 +0100
    31.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jul 27 22:08:46 2015 +0200
    31.3 @@ -690,7 +690,7 @@
    31.4              (map Logic.varifyT_global As ~~ As);
    31.5  
    31.6          fun inst_thm t thm =
    31.7 -          Drule.instantiate' [] [SOME (Thm.cterm_of lthy t)]
    31.8 +          Thm.instantiate' [] [SOME (Thm.cterm_of lthy t)]
    31.9              (Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm));
   31.10  
   31.11          val uexhaust_thm = inst_thm u exhaust_thm;
    32.1 --- a/src/HOL/Tools/Function/function_context_tree.ML	Mon Jul 27 16:52:57 2015 +0100
    32.2 +++ b/src/HOL/Tools/Function/function_context_tree.ML	Mon Jul 27 22:08:46 2015 +0200
    32.3 @@ -248,7 +248,7 @@
    32.4            val iha = import_thm ctxt (fix, h_as) ha (* (a', h a') : G *)
    32.5              |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
    32.6                                                      (* (a, h a) : G   *)
    32.7 -          val inst_ih = instantiate' [] [SOME (Thm.cterm_of ctxt arg)] ih
    32.8 +          val inst_ih = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt arg)] ih
    32.9            val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
   32.10  
   32.11            val h_a'_eq_h_a = Thm.combination (Thm.reflexive (Thm.cterm_of ctxt h)) inner
    33.1 --- a/src/HOL/Tools/Function/function_core.ML	Mon Jul 27 16:52:57 2015 +0100
    33.2 +++ b/src/HOL/Tools/Function/function_core.ML	Mon Jul 27 22:08:46 2015 +0200
    33.3 @@ -371,7 +371,7 @@
    33.4  
    33.5      val exactly_one =
    33.6        @{thm ex1I}
    33.7 -      |> instantiate'
    33.8 +      |> Thm.instantiate'
    33.9            [SOME (Thm.ctyp_of ctxt ranT)]
   33.10            [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
   33.11        |> curry (op COMP) existence
   33.12 @@ -407,7 +407,7 @@
   33.13      val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
   33.14      val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
   33.15      val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
   33.16 -      |> instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
   33.17 +      |> Thm.instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
   33.18  
   33.19      val _ = trace_msg (K "Proving Replacement lemmas...")
   33.20      val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses
   33.21 @@ -694,7 +694,7 @@
   33.22        |> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
   33.23        |> assume_tac ctxt 1 |> Seq.hd
   33.24        |> (curry op COMP) (acc_downward
   33.25 -        |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
   33.26 +        |> (Thm.instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
   33.27          |> Thm.forall_intr (Thm.cterm_of ctxt z)
   33.28          |> Thm.forall_intr (Thm.cterm_of ctxt x))
   33.29        |> Thm.forall_intr (Thm.cterm_of ctxt a)
    34.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Mon Jul 27 16:52:57 2015 +0100
    34.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Mon Jul 27 22:08:46 2015 +0200
    34.3 @@ -374,7 +374,7 @@
    34.4            |> Thm.cterm_of ctxt''
    34.5        in
    34.6          indthm
    34.7 -        |> Drule.instantiate' [] [SOME inst]
    34.8 +        |> Thm.instantiate' [] [SOME inst]
    34.9          |> simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt'')
   34.10          |> Conv.fconv_rule (ind_rulify ctxt'')
   34.11        end
    35.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Mon Jul 27 16:52:57 2015 +0100
    35.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Mon Jul 27 22:08:46 2015 +0200
    35.3 @@ -278,7 +278,7 @@
    35.4           THEN (resolve_tac ctxt @{thms reduction_pair_lemma} 1)
    35.5           THEN (resolve_tac ctxt @{thms rp_inv_image_rp} 1)
    35.6           THEN (resolve_tac ctxt [order_rpair ms_rp label] 1)
    35.7 -         THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
    35.8 +         THEN PRIMITIVE (Thm.instantiate' [] [SOME level_mapping])
    35.9           THEN unfold_tac ctxt @{thms rp_inv_image_def}
   35.10           THEN Local_Defs.unfold_tac ctxt @{thms split_conv fst_conv snd_conv}
   35.11           THEN REPEAT (SOMEGOAL (resolve_tac ctxt [@{thm Un_least}, @{thm empty_subsetI}]))
    36.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon Jul 27 16:52:57 2015 +0100
    36.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Mon Jul 27 22:08:46 2015 +0200
    36.3 @@ -409,7 +409,7 @@
    36.4        then 
    36.5          let 
    36.6            val instantiated_id_quot_thm =
    36.7 -            instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
    36.8 +            Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
    36.9          in
   36.10            (instantiated_id_quot_thm, (table, ctxt)) 
   36.11          end
    37.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon Jul 27 16:52:57 2015 +0100
    37.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Jul 27 22:08:46 2015 +0200
    37.3 @@ -173,7 +173,7 @@
    37.4      let
    37.5        val cc = Thm.cterm_of ctxt c
    37.6        val ct = Thm.dest_arg (Thm.cprop_of th)
    37.7 -    in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    37.8 +    in resolve_tac ctxt [th] i (Thm.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    37.9    | _ => resolve_tac ctxt [th] i st
   37.10  
   37.11  (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
    38.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon Jul 27 16:52:57 2015 +0100
    38.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Mon Jul 27 22:08:46 2015 +0200
    38.3 @@ -102,13 +102,13 @@
    38.4        val cxT = Thm.ctyp_of ctxt xT
    38.5        val cbodyT = Thm.ctyp_of ctxt bodyT
    38.6        fun makeK () =
    38.7 -        instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.cterm_of ctxt body)] @{thm abs_K}
    38.8 +        Thm.instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.cterm_of ctxt body)] @{thm abs_K}
    38.9    in
   38.10        case body of
   38.11            Const _ => makeK()
   38.12          | Free _ => makeK()
   38.13          | Var _ => makeK()  (*though Var isn't expected*)
   38.14 -        | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
   38.15 +        | Bound 0 => Thm.instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
   38.16          | rator$rand =>
   38.17              if Term.is_dependent rator then (*C or S*)
   38.18                 if Term.is_dependent rand then (*S*)
    39.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jul 27 16:52:57 2015 +0100
    39.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jul 27 22:08:46 2015 +0200
    39.3 @@ -50,7 +50,7 @@
    39.4      let
    39.5        val ct = Thm.cterm_of ctxt t
    39.6        val cT = Thm.ctyp_of_cterm ct
    39.7 -    in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
    39.8 +    in refl |> Thm.instantiate' [SOME cT] [SOME ct] end
    39.9    | Const (@{const_name disj}, _) $ t1 $ t2 =>
   39.10      (if can HOLogic.dest_not t1 then t2 else t1)
   39.11      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
    40.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Jul 27 16:52:57 2015 +0100
    40.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Jul 27 22:08:46 2015 +0200
    40.3 @@ -397,7 +397,7 @@
    40.4      (* prove  inj Rep_dt_i  and  Rep_dt_i x : rep_set_dt_i *)
    40.5  
    40.6      val fun_congs =
    40.7 -      map (fn T => make_elim (Drule.instantiate' [SOME (Thm.global_ctyp_of thy5 T)] [] fun_cong)) branchTs;
    40.8 +      map (fn T => make_elim (Thm.instantiate' [SOME (Thm.global_ctyp_of thy5 T)] [] fun_cong)) branchTs;
    40.9  
   40.10      fun prove_iso_thms ds (inj_thms, elem_thms) =
   40.11        let
    41.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Jul 27 16:52:57 2015 +0100
    41.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Jul 27 22:08:46 2015 +0200
    41.3 @@ -84,17 +84,17 @@
    41.4  val is_number = can dest_number;
    41.5  
    41.6  val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
    41.7 -    map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
    41.8 +    map (Thm.instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
    41.9  
   41.10  val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =
   41.11 -    map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
   41.12 +    map (Thm.instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
   41.13  
   41.14  val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] =
   41.15 -    map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
   41.16 +    map (Thm.instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
   41.17  
   41.18 -val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
   41.19 +val [miP, piP] = map (Thm.instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
   41.20  
   41.21 -val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
   41.22 +val infDP = Thm.instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
   41.23  
   41.24  val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,
   41.25        asetgt, asetge, asetdvd, asetndvd,asetP],
   41.26 @@ -103,7 +103,7 @@
   41.27  
   41.28  val [cpmi, cppi] = [@{thm "cpmi"}, @{thm "cppi"}];
   41.29  
   41.30 -val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
   41.31 +val unity_coeff_ex = Thm.instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
   41.32  
   41.33  val [zdvd_mono,simp_from_to,all_not_ex] =
   41.34       [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
   41.35 @@ -166,9 +166,9 @@
   41.36    in (mi_th, set_th, infD_th)
   41.37    end;
   41.38  
   41.39 -val inst' = fn cts => instantiate' [] (map SOME cts);
   41.40 -val infDTrue = instantiate' [] [SOME true_tm] infDP;
   41.41 -val infDFalse = instantiate' [] [SOME false_tm] infDP;
   41.42 +val inst' = fn cts => Thm.instantiate' [] (map SOME cts);
   41.43 +val infDTrue = Thm.instantiate' [] [SOME true_tm] infDP;
   41.44 +val infDFalse = Thm.instantiate' [] [SOME false_tm] infDP;
   41.45  
   41.46  val cadd =  @{cterm "op + :: int => _"}
   41.47  val cmulC =  @{cterm "op * :: int => _"}
   41.48 @@ -483,16 +483,16 @@
   41.49     in Thm.equal_elim (Thm.symmetric th) TrueI end;
   41.50      (* A and B set *)
   41.51     local
   41.52 -     val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
   41.53 -     val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
   41.54 +     val insI1 = Thm.instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
   41.55 +     val insI2 = Thm.instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
   41.56     in
   41.57      fun provein x S =
   41.58       case Thm.term_of S of
   41.59          Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
   41.60        | Const(@{const_name insert}, _) $ y $ _ =>
   41.61           let val (cy,S') = Thm.dest_binop S
   41.62 -         in if Thm.term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
   41.63 -         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   41.64 +         in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1
   41.65 +         else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2)
   41.66                             (provein x S')
   41.67           end
   41.68     end
   41.69 @@ -519,7 +519,7 @@
   41.70    let
   41.71     val sths = map (fn (tl,t0) =>
   41.72                        if tl = Thm.term_of t0
   41.73 -                      then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
   41.74 +                      then Thm.instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
   41.75                        else provelin ctxt ((HOLogic.eq_const iT)$tl$(Thm.term_of t0)
   41.76                                   |> HOLogic.mk_Trueprop))
   41.77                     (sl ~~ s0)
   41.78 @@ -527,7 +527,7 @@
   41.79     val S = mkISet csl
   41.80     val inStab = fold (fn ct => fn tab => Termtab.update (Thm.term_of ct, provein ct S) tab)
   41.81                      csl Termtab.empty
   41.82 -   val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
   41.83 +   val eqelem_th = Thm.instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
   41.84     val inS =
   41.85       let
   41.86        val tab = fold Termtab.update
   41.87 @@ -536,7 +536,7 @@
   41.88                      val th =
   41.89                        if s aconvc t
   41.90                        then the (Termtab.lookup inStab (Thm.term_of s))
   41.91 -                      else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
   41.92 +                      else FWD (Thm.instantiate' [] [SOME s, SOME t] eqelem_th)
   41.93                          [eq, the (Termtab.lookup inStab (Thm.term_of s))]
   41.94                   in (Thm.term_of t, th) end) sths) Termtab.empty
   41.95          in
   41.96 @@ -801,7 +801,7 @@
   41.97  
   41.98  fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
   41.99   let 
  41.100 -   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
  41.101 +   fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"}
  41.102     fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
  41.103     val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
  41.104     val p' = fold_rev gen ts p
    42.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Mon Jul 27 16:52:57 2015 +0100
    42.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Mon Jul 27 22:08:46 2015 +0200
    42.3 @@ -45,7 +45,7 @@
    42.4      let
    42.5       val p = Thm.dest_arg p
    42.6       val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
    42.7 -     val th = instantiate' [SOME T] [SOME p] all_not_ex
    42.8 +     val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex
    42.9      in Thm.transitive th (conv env (Thm.rhs_of th))
   42.10      end
   42.11    | _ => atcv env p
    43.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 27 16:52:57 2015 +0100
    43.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 27 22:08:46 2015 +0200
    43.3 @@ -80,7 +80,7 @@
    43.4      val cty = Thm.global_ctyp_of thy ty;
    43.5    in
    43.6      @{thm partial_term_of_anything}
    43.7 -    |> Drule.instantiate' [SOME cty] insts
    43.8 +    |> Thm.instantiate' [SOME cty] insts
    43.9      |> Thm.varifyT_global
   43.10    end
   43.11  
   43.12 @@ -99,7 +99,7 @@
   43.13            @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
   43.14      val var_eq =
   43.15        @{thm partial_term_of_anything}
   43.16 -      |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
   43.17 +      |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
   43.18        |> Thm.varifyT_global
   43.19      val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs;
   43.20   in
    44.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Jul 27 16:52:57 2015 +0100
    44.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Jul 27 22:08:46 2015 +0200
    44.3 @@ -99,7 +99,7 @@
    44.4      val ty_inst = map (SOME o Thm.ctyp_of ctxt) [domain_type (fastype_of R2)]
    44.5      val trm_inst = map (SOME o Thm.cterm_of ctxt) [R2, R1]
    44.6    in
    44.7 -    (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
    44.8 +    (case try (Thm.instantiate' ty_inst trm_inst) ball_bex_thm of
    44.9        NONE => NONE
   44.10      | SOME thm' =>
   44.11          (case try (get_match_inst thy (get_lhs thm')) redex of
   44.12 @@ -198,7 +198,7 @@
   44.13          val cfx = Thm.cterm_of ctxt fx;
   44.14          val cxt = Thm.ctyp_of ctxt (fastype_of x);
   44.15          val cfxt = Thm.ctyp_of ctxt (fastype_of fx);
   44.16 -        val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
   44.17 +        val thm = Thm.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
   44.18        in
   44.19          Conv.rewr_conv thm ctrm
   44.20        end)
   44.21 @@ -247,7 +247,7 @@
   44.22                val ty_f = range_type (fastype_of f)
   44.23                val ty_inst = map (SOME o Thm.ctyp_of ctxt) [ty_x, ty_b, ty_f]
   44.24                val t_inst = map (SOME o Thm.cterm_of ctxt) [R2, f, g, x, y];
   44.25 -              val inst_thm = Drule.instantiate' ty_inst
   44.26 +              val inst_thm = Thm.instantiate' ty_inst
   44.27                  ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
   44.28              in
   44.29                (resolve_tac ctxt [inst_thm] THEN' SOLVED' (quotient_tac ctxt)) 1
   44.30 @@ -264,7 +264,7 @@
   44.31        let
   44.32          val ty = domain_type (fastype_of R)
   44.33        in
   44.34 -        case try (Drule.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
   44.35 +        case try (Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
   44.36              [SOME (Thm.cterm_of ctxt R)]) @{thm equals_rsp} of
   44.37            SOME thm => resolve_tac ctxt [thm] THEN' quotient_tac ctxt
   44.38          | NONE => K no_tac
   44.39 @@ -281,7 +281,7 @@
   44.40          in
   44.41            case try (map (SOME o Thm.cterm_of ctxt)) [rel, abs, rep] of
   44.42              SOME t_inst =>
   44.43 -              (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
   44.44 +              (case try (Thm.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
   44.45                  SOME inst_thm => (resolve_tac ctxt [inst_thm] THEN' quotient_tac ctxt) i
   44.46                | NONE => no_tac)
   44.47            | NONE => no_tac
   44.48 @@ -468,7 +468,7 @@
   44.49          val (ty_c, ty_d) = dest_funT (fastype_of a2)
   44.50          val tyinst = map (SOME o Thm.ctyp_of ctxt) [ty_a, ty_b, ty_c, ty_d]
   44.51          val tinst = [NONE, NONE, SOME (Thm.cterm_of ctxt r1), NONE, SOME (Thm.cterm_of ctxt a2)]
   44.52 -        val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
   44.53 +        val thm1 = Thm.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
   44.54          val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
   44.55          val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
   44.56          val (insp, inst) =
   44.57 @@ -529,7 +529,7 @@
   44.58  (* Tactic for Generalising Free Variables in a Goal *)
   44.59  
   44.60  fun inst_spec ctrm =
   44.61 -  Drule.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec}
   44.62 +  Thm.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec}
   44.63  
   44.64  fun inst_spec_tac ctxt ctrms =
   44.65    EVERY' (map (dresolve_tac ctxt o single o inst_spec) ctrms)
   44.66 @@ -602,7 +602,7 @@
   44.67      val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
   44.68        handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   44.69    in
   44.70 -    Drule.instantiate' []
   44.71 +    Thm.instantiate' []
   44.72        [SOME (Thm.cterm_of ctxt rtrm'),
   44.73         SOME (Thm.cterm_of ctxt reg_goal),
   44.74         NONE,
   44.75 @@ -661,7 +661,7 @@
   44.76      val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
   44.77        handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   44.78    in
   44.79 -    Drule.instantiate' []
   44.80 +    Thm.instantiate' []
   44.81        [SOME (Thm.cterm_of ctxt reg_goal),
   44.82         NONE,
   44.83         SOME (Thm.cterm_of ctxt inj_goal)] partiality_procedure_thm
    45.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Mon Jul 27 16:52:57 2015 +0100
    45.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Mon Jul 27 22:08:46 2015 +0200
    45.3 @@ -218,7 +218,7 @@
    45.4  fun Rel_conv ct =
    45.5    let val (cT, cT') = dest_funcT (Thm.ctyp_of_cterm ct)
    45.6        val (cU, _) = dest_funcT cT'
    45.7 -  in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
    45.8 +  in Thm.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
    45.9  
   45.10  (* Conversion to preprocess a transfer rule *)
   45.11  fun safe_Rel_conv ct =
   45.12 @@ -463,7 +463,7 @@
   45.13              val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
   45.14              val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
   45.15              val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
   45.16 -            val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
   45.17 +            val rule = Thm.instantiate' tinsts insts @{thm Rel_abs}
   45.18              val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
   45.19            in
   45.20              (thm2 COMP rule, hyps)
    46.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Jul 27 16:52:57 2015 +0100
    46.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Jul 27 22:08:46 2015 +0200
    46.3 @@ -359,7 +359,7 @@
    46.4          val kill_True = Local_Defs.unfold lthy [@{thm HOL.simp_thms(21)}]
    46.5        in
    46.6          thm
    46.7 -        |> Drule.instantiate' cTs cts
    46.8 +        |> Thm.instantiate' cTs cts
    46.9          |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
   46.10            (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
   46.11          |> Local_Defs.unfold lthy eq_onps
    47.1 --- a/src/HOL/Tools/choice_specification.ML	Mon Jul 27 16:52:57 2015 +0100
    47.2 +++ b/src/HOL/Tools/choice_specification.ML	Mon Jul 27 22:08:46 2015 +0200
    47.3 @@ -138,7 +138,7 @@
    47.4            let
    47.5              val cv = Thm.global_cterm_of thy v
    47.6              val cT = Thm.ctyp_of_cterm cv
    47.7 -            val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec
    47.8 +            val spec' = Thm.instantiate' [SOME cT] [NONE, SOME cv] spec
    47.9            in thm RS spec' end
   47.10          fun remove_alls frees (thm, thy) = (fold (inst_all thy) frees thm, thy)
   47.11          fun process_single ((name, atts), rew_imp, frees) args =
    48.1 --- a/src/HOL/Tools/cnf.ML	Mon Jul 27 16:52:57 2015 +0100
    48.2 +++ b/src/HOL/Tools/cnf.ML	Mon Jul 27 22:08:46 2015 +0200
    48.3 @@ -165,7 +165,7 @@
    48.4  (* ------------------------------------------------------------------------- *)
    48.5  
    48.6  fun inst_thm thy ts thm =
    48.7 -  instantiate' [] (map (SOME o Thm.global_cterm_of thy) ts) thm;
    48.8 +  Thm.instantiate' [] (map (SOME o Thm.global_cterm_of thy) ts) thm;
    48.9  
   48.10  (* ------------------------------------------------------------------------- *)
   48.11  (*                         Naive CNF transformation                          *)
    49.1 --- a/src/HOL/Tools/code_evaluation.ML	Mon Jul 27 16:52:57 2015 +0100
    49.2 +++ b/src/HOL/Tools/code_evaluation.ML	Mon Jul 27 22:08:46 2015 +0200
    49.3 @@ -69,7 +69,7 @@
    49.4      val cty = Thm.global_ctyp_of thy ty;
    49.5    in
    49.6      @{thm term_of_anything}
    49.7 -    |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    49.8 +    |> Thm.instantiate' [SOME cty] [SOME arg, SOME rhs]
    49.9      |> Thm.varifyT_global
   49.10    end;
   49.11  
   49.12 @@ -106,7 +106,7 @@
   49.13      val cty = Thm.global_ctyp_of thy ty;
   49.14    in
   49.15      @{thm term_of_anything}
   49.16 -    |> Drule.instantiate' [SOME cty] [SOME (Thm.global_cterm_of thy arg), SOME rhs]
   49.17 +    |> Thm.instantiate' [SOME cty] [SOME (Thm.global_cterm_of thy arg), SOME rhs]
   49.18      |> Thm.varifyT_global
   49.19    end;
   49.20  
    50.1 --- a/src/HOL/Tools/groebner.ML	Mon Jul 27 16:52:57 2015 +0100
    50.2 +++ b/src/HOL/Tools/groebner.ML	Mon Jul 27 22:08:46 2015 +0200
    50.3 @@ -413,7 +413,7 @@
    50.4  fun initial_conv ctxt =
    50.5    Simplifier.rewrite (put_simpset initial_ss ctxt);
    50.6  
    50.7 -val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
    50.8 +val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
    50.9  
   50.10  val cTrp = @{cterm "Trueprop"};
   50.11  val cConj = @{cterm HOL.conj};
   50.12 @@ -435,7 +435,7 @@
   50.13  
   50.14  fun sym_conv eq =
   50.15   let val (l,r) = Thm.dest_binop eq
   50.16 - in instantiate' [SOME (Thm.ctyp_of_cterm l)] [SOME l, SOME r] eq_commute
   50.17 + in Thm.instantiate' [SOME (Thm.ctyp_of_cterm l)] [SOME l, SOME r] eq_commute
   50.18   end;
   50.19  
   50.20    (* FIXME : copied from cqe.ML -- complex QE*)
   50.21 @@ -471,14 +471,14 @@
   50.22    fun tabr c = the (Termtab.lookup ctabr (Thm.term_of c))
   50.23    val thl  = prove_conj tabl (conjuncts r) |> implies_intr_hyps
   50.24    val thr  = prove_conj tabr (conjuncts l) |> implies_intr_hyps
   50.25 -  val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI}
   50.26 +  val eqI = Thm.instantiate' [] [SOME l, SOME r] @{thm iffI}
   50.27   in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
   50.28  
   50.29   (* END FIXME.*)
   50.30  
   50.31     (* Conversion for the equivalence of existential statements where
   50.32        EX quantifiers are rearranged differently *)
   50.33 - fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   50.34 + fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
   50.35   fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
   50.36  
   50.37  fun choose v th th' = case Thm.concl_of th of
   50.38 @@ -487,7 +487,7 @@
   50.39      val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
   50.40      val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
   50.41      val th0 = Conv.fconv_rule (Thm.beta_conversion true)
   50.42 -        (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   50.43 +        (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   50.44      val pv = (Thm.rhs_of o Thm.beta_conversion true)
   50.45            (Thm.apply @{cterm Trueprop} (Thm.apply p v))
   50.46      val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
   50.47 @@ -504,7 +504,7 @@
   50.48     val p = Thm.lambda v (Thm.dest_arg (Thm.cprop_of th))
   50.49    in Thm.implies_elim
   50.50      (Conv.fconv_rule (Thm.beta_conversion true)
   50.51 -      (instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI}))
   50.52 +      (Thm.instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI}))
   50.53        th
   50.54    end
   50.55   fun ex_eq_conv t =
   50.56 @@ -517,7 +517,7 @@
   50.57     val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th))
   50.58     val p = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) th1
   50.59     val q = (Thm.dest_arg o Thm.dest_arg o Thm.cprop_of) th1
   50.60 -  in Thm.implies_elim (Thm.implies_elim (instantiate' [] [SOME p, SOME q] iffI) th1) th2
   50.61 +  in Thm.implies_elim (Thm.implies_elim (Thm.instantiate' [] [SOME p, SOME q] iffI) th1) th2
   50.62       |> mk_meta_eq
   50.63    end;
   50.64  
   50.65 @@ -739,7 +739,7 @@
   50.66   let
   50.67    fun mk_forall x p =
   50.68      Thm.apply
   50.69 -      (Drule.cterm_rule (instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
   50.70 +      (Drule.cterm_rule (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
   50.71          @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
   50.72    val avs = Thm.add_cterm_frees tm []
   50.73    val P' = fold mk_forall avs tm
   50.74 @@ -775,7 +775,7 @@
   50.75  fun poly_eq_conv t =
   50.76   let val (a,b) = Thm.dest_binop t
   50.77   in Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv ring_normalize_conv))
   50.78 -     (instantiate' [] [SOME a, SOME b] idl_sub)
   50.79 +     (Thm.instantiate' [] [SOME a, SOME b] idl_sub)
   50.80   end
   50.81   val poly_eq_simproc =
   50.82    let
   50.83 @@ -810,7 +810,7 @@
   50.84     | NONE => (the (find_first
   50.85            (fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th)
   50.86     val th2 = Thm.transitive th1
   50.87 -        (instantiate' []  [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v]
   50.88 +        (Thm.instantiate' []  [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v]
   50.89            idl_add0)
   50.90     in Conv.fconv_rule(funpow 2 Conv.arg_conv ring_normalize_conv) th2
   50.91     end
   50.92 @@ -946,7 +946,7 @@
   50.93   | _=> raise CTERM ("ideal_tac - lhs",[t])
   50.94   fun exitac _ NONE = no_tac
   50.95     | exitac ctxt (SOME y) =
   50.96 -      resolve_tac ctxt [instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1
   50.97 +      resolve_tac ctxt [Thm.instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1
   50.98  
   50.99   val claset = claset_of @{context}
  50.100  in
    51.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Jul 27 16:52:57 2015 +0100
    51.2 +++ b/src/HOL/Tools/inductive_set.ML	Mon Jul 27 22:08:46 2015 +0200
    51.3 @@ -42,7 +42,7 @@
    51.4      let
    51.5        fun close p t f =
    51.6          let val vs = Term.add_vars t []
    51.7 -        in Drule.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
    51.8 +        in Thm.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
    51.9            (p (fold (Logic.all o Var) vs t) f)
   51.10          end;
   51.11        fun mkop @{const_name HOL.conj} T x =
    52.1 --- a/src/HOL/Tools/int_arith.ML	Mon Jul 27 16:52:57 2015 +0100
    52.2 +++ b/src/HOL/Tools/int_arith.ML	Mon Jul 27 22:08:46 2015 +0200
    52.3 @@ -27,7 +27,7 @@
    52.4  fun proc0 phi ctxt ct =
    52.5    let val T = Thm.ctyp_of_cterm ct
    52.6    in if Thm.typ_of T = @{typ int} then NONE else
    52.7 -     SOME (instantiate' [SOME T] [] zeroth)
    52.8 +     SOME (Thm.instantiate' [SOME T] [] zeroth)
    52.9    end;
   52.10  
   52.11  val zero_to_of_int_zero_simproc =
   52.12 @@ -41,7 +41,7 @@
   52.13  fun proc1 phi ctxt ct =
   52.14    let val T = Thm.ctyp_of_cterm ct
   52.15    in if Thm.typ_of T = @{typ int} then NONE else
   52.16 -     SOME (instantiate' [SOME T] [] oneth)
   52.17 +     SOME (Thm.instantiate' [SOME T] [] oneth)
   52.18    end;
   52.19  
   52.20  val one_to_of_int_one_simproc =
    53.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Mon Jul 27 16:52:57 2015 +0100
    53.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Jul 27 22:08:46 2015 +0200
    53.3 @@ -610,7 +610,7 @@
    53.4      val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z,w]
    53.5      val T = Thm.ctyp_of_cterm x
    53.6      val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z]
    53.7 -    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
    53.8 +    val th = Thm.instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
    53.9    in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz)
   53.10    end
   53.11    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
   53.12 @@ -624,13 +624,13 @@
   53.13          let val (x,y) = Thm.dest_binop l val z = r
   53.14              val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
   53.15              val ynz = prove_nz ctxt T y
   53.16 -        in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
   53.17 +        in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
   53.18          end
   53.19       | (_, Const (@{const_name Rings.divide},_)$_$_) =>
   53.20          let val (x,y) = Thm.dest_binop r val z = l
   53.21              val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
   53.22              val ynz = prove_nz ctxt T y
   53.23 -        in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
   53.24 +        in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
   53.25          end
   53.26       | _ => NONE)
   53.27    end
   53.28 @@ -648,42 +648,42 @@
   53.29          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   53.30          val _ = map is_number [a,b,c]
   53.31          val T = Thm.ctyp_of_cterm c
   53.32 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
   53.33 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
   53.34        in SOME (mk_meta_eq th) end
   53.35    | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   53.36        let
   53.37          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   53.38          val _ = map is_number [a,b,c]
   53.39          val T = Thm.ctyp_of_cterm c
   53.40 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
   53.41 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
   53.42        in SOME (mk_meta_eq th) end
   53.43    | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
   53.44        let
   53.45          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
   53.46          val _ = map is_number [a,b,c]
   53.47          val T = Thm.ctyp_of_cterm c
   53.48 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
   53.49 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
   53.50        in SOME (mk_meta_eq th) end
   53.51    | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   53.52      let
   53.53        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   53.54          val _ = map is_number [a,b,c]
   53.55          val T = Thm.ctyp_of_cterm c
   53.56 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
   53.57 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
   53.58        in SOME (mk_meta_eq th) end
   53.59    | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   53.60      let
   53.61        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   53.62          val _ = map is_number [a,b,c]
   53.63          val T = Thm.ctyp_of_cterm c
   53.64 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   53.65 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
   53.66        in SOME (mk_meta_eq th) end
   53.67    | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
   53.68      let
   53.69        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
   53.70          val _ = map is_number [a,b,c]
   53.71          val T = Thm.ctyp_of_cterm c
   53.72 -        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
   53.73 +        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
   53.74        in SOME (mk_meta_eq th) end
   53.75    | _ => NONE)
   53.76    handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
    54.1 --- a/src/HOL/Tools/record.ML	Mon Jul 27 16:52:57 2015 +0100
    54.2 +++ b/src/HOL/Tools/record.ML	Mon Jul 27 22:08:46 2015 +0200
    54.3 @@ -85,7 +85,7 @@
    54.4    let
    54.5      val exists_thm =
    54.6        UNIV_I
    54.7 -      |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type))] [];
    54.8 +      |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type))] [];
    54.9      val proj_constr = Abs_inverse OF [exists_thm];
   54.10      val absT = Type (tyco, map TFree vs);
   54.11    in
    55.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Mon Jul 27 16:52:57 2015 +0100
    55.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Mon Jul 27 22:08:46 2015 +0200
    55.3 @@ -142,7 +142,7 @@
    55.4        let val (a, b) = Rat.quotient_of_rat x
    55.5        in if b = 1 then Numeral.mk_cnumber cT a
    55.6          else Thm.apply
    55.7 -             (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
    55.8 +             (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"})
    55.9                           (Numeral.mk_cnumber cT a))
   55.10               (Numeral.mk_cnumber cT b)
   55.11        end
    56.1 --- a/src/Pure/axclass.ML	Mon Jul 27 16:52:57 2015 +0100
    56.2 +++ b/src/Pure/axclass.ML	Mon Jul 27 22:08:46 2015 +0200
    56.3 @@ -191,7 +191,7 @@
    56.4                thy2
    56.5                |> update_classrel ((c1, c2),
    56.6                  (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
    56.7 -                |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
    56.8 +                |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
    56.9                  |> Thm.close_derivation));
   56.10  
   56.11          val proven = is_classrel thy1;
   56.12 @@ -234,7 +234,7 @@
   56.13        let
   56.14          val th1 =
   56.15            (th RS the_classrel thy (c, c1))
   56.16 -          |> Drule.instantiate' std_vars []
   56.17 +          |> Thm.instantiate' std_vars []
   56.18            |> Thm.close_derivation;
   56.19        in ((th1, thy_name), c1) end);
   56.20  
   56.21 @@ -396,7 +396,7 @@
   56.22      val (th', thy') = Global_Theory.store_thm (binding, th) thy;
   56.23      val th'' = th'
   56.24        |> Thm.unconstrainT
   56.25 -      |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
   56.26 +      |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
   56.27    in
   56.28      thy'
   56.29      |> Sign.primitive_classrel (c1, c2)
   56.30 @@ -426,7 +426,7 @@
   56.31        |> (map o apsnd o map_atyps) (K T);
   56.32      val th'' = th'
   56.33        |> Thm.unconstrainT
   56.34 -      |> Drule.instantiate' std_vars [];
   56.35 +      |> Thm.instantiate' std_vars [];
   56.36    in
   56.37      thy'
   56.38      |> fold (#2 oo declare_overloaded) missing_params
    57.1 --- a/src/Pure/drule.ML	Mon Jul 27 16:52:57 2015 +0100
    57.2 +++ b/src/Pure/drule.ML	Mon Jul 27 22:08:46 2015 +0200
    57.3 @@ -24,7 +24,6 @@
    57.4      thm -> thm
    57.5    val infer_instantiate_types: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm
    57.6    val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
    57.7 -  val instantiate': ctyp option list -> cterm option list -> thm -> thm
    57.8    val infer_instantiate': Proof.context -> cterm option list -> thm -> thm
    57.9    val zero_var_indexes_list: thm list -> thm list
   57.10    val zero_var_indexes: thm -> thm
   57.11 @@ -798,26 +797,6 @@
   57.12            AList.lookup (op =) vars xi |> Option.map (fn T => ((xi, T), cu)));
   57.13        in infer_instantiate_types ctxt args' th end;
   57.14  
   57.15 -
   57.16 -(* instantiate by left-to-right occurrence of variables *)
   57.17 -
   57.18 -fun instantiate' cTs cts thm =
   57.19 -  let
   57.20 -    fun err msg =
   57.21 -      raise TYPE ("instantiate': " ^ msg,
   57.22 -        map_filter (Option.map Thm.typ_of) cTs,
   57.23 -        map_filter (Option.map Thm.term_of) cts);
   57.24 -
   57.25 -    fun zip_vars xs ys =
   57.26 -      zip_options xs ys handle ListPair.UnequalLengths =>
   57.27 -        err "more instantiations than variables in thm";
   57.28 -
   57.29 -    val thm' =
   57.30 -      Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
   57.31 -    val thm'' =
   57.32 -      Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
   57.33 -  in thm'' end;
   57.34 -
   57.35  fun infer_instantiate' ctxt args th =
   57.36    let
   57.37      val vars = rev (Term.add_vars (Thm.full_prop_of th) []);
    58.1 --- a/src/Pure/more_thm.ML	Mon Jul 27 16:52:57 2015 +0100
    58.2 +++ b/src/Pure/more_thm.ML	Mon Jul 27 22:08:46 2015 +0200
    58.3 @@ -60,6 +60,7 @@
    58.4    val elim_implies: thm -> thm -> thm
    58.5    val forall_elim_var: int -> thm -> thm
    58.6    val forall_elim_vars: int -> thm -> thm
    58.7 +  val instantiate': ctyp option list -> cterm option list -> thm -> thm
    58.8    val global_certify_inst: theory ->
    58.9      ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
   58.10      ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   58.11 @@ -354,6 +355,26 @@
   58.12  end;
   58.13  
   58.14  
   58.15 +(* instantiate by left-to-right occurrence of variables *)
   58.16 +
   58.17 +fun instantiate' cTs cts thm =
   58.18 +  let
   58.19 +    fun err msg =
   58.20 +      raise TYPE ("instantiate': " ^ msg,
   58.21 +        map_filter (Option.map Thm.typ_of) cTs,
   58.22 +        map_filter (Option.map Thm.term_of) cts);
   58.23 +
   58.24 +    fun zip_vars xs ys =
   58.25 +      zip_options xs ys handle ListPair.UnequalLengths =>
   58.26 +        err "more instantiations than variables in thm";
   58.27 +
   58.28 +    val thm' =
   58.29 +      Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
   58.30 +    val thm'' =
   58.31 +      Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
   58.32 +  in thm'' end;
   58.33 +
   58.34 +
   58.35  (* certify_instantiate *)
   58.36  
   58.37  fun global_certify_inst thy (instT, inst) =
    59.1 --- a/src/Tools/atomize_elim.ML	Mon Jul 27 16:52:57 2015 +0100
    59.2 +++ b/src/Tools/atomize_elim.ML	Mon Jul 27 22:08:46 2015 +0200
    59.3 @@ -117,7 +117,7 @@
    59.4            if is_Bound thesis then all_tac
    59.5            else let
    59.6                val cthesis = Thm.global_cterm_of thy thesis
    59.7 -              val rule = instantiate' [SOME (Thm.ctyp_of_cterm cthesis)] [NONE, SOME cthesis]
    59.8 +              val rule = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cthesis)] [NONE, SOME cthesis]
    59.9                           @{thm meta_spec}
   59.10              in
   59.11                compose_tac ctxt (false, rule, 1) i