--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Jul 27 17:44:55 2015 +0200
@@ -906,7 +906,7 @@
let val (a, b) = Rat.quotient_of_rat x
in if b = 1 then Numeral.mk_cnumber cT a
else Thm.apply
- (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
+ (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"})
(Numeral.mk_cnumber cT a))
(Numeral.mk_cnumber cT b)
end
@@ -939,7 +939,7 @@
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
- val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
+ val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
(if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
@@ -947,7 +947,7 @@
| ("x+t",[t]) =>
let
val T = Thm.ctyp_of_cterm x
- val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
+ val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
in rth end
@@ -962,7 +962,7 @@
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
- val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
+ val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
(if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
val rth = th
in rth end
@@ -975,7 +975,7 @@
let
val T = Thm.ctyp_of_cterm x
val cr = dest_frac c
- val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
+ val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"}
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
val cthp = Simplifier.rewrite ctxt
@@ -983,7 +983,7 @@
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
- val th = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
+ val th = Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [c,x,t])
(if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
@@ -991,7 +991,7 @@
| ("x+t",[t]) =>
let
val T = Thm.ctyp_of_cterm x
- val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
+ val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
in rth end
@@ -999,7 +999,7 @@
let
val T = Thm.ctyp_of_cterm x
val cr = dest_frac c
- val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
+ val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"}
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
val cthp = Simplifier.rewrite ctxt
@@ -1007,7 +1007,7 @@
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
- val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
+ val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
(if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
val rth = th
in rth end
@@ -1026,14 +1026,14 @@
(Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim
- (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
+ (Thm.instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
in rth end
| ("x+t",[t]) =>
let
val T = Thm.ctyp_of_cterm x
- val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
+ val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
in rth end
@@ -1048,7 +1048,7 @@
(Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val rth = Thm.implies_elim
- (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
+ (Thm.instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
in rth end
| _ => Thm.reflexive ct);
@@ -1062,7 +1062,7 @@
Const(@{const_name Orderings.less},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm ca
- val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
+ val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
(Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
@@ -1071,7 +1071,7 @@
| Const(@{const_name Orderings.less_eq},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm ca
- val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
+ val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
(Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
@@ -1081,7 +1081,7 @@
| Const(@{const_name HOL.eq},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm ca
- val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
+ val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
(Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Mon Jul 27 17:44:55 2015 +0200
@@ -96,7 +96,7 @@
val cring_ctxt = ctxt addsimps cring_simps; (*FIXME really the full simpset!?*)
val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g);
val norm_eq_th = (* may collapse to True *)
- simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
+ simplify cring_ctxt (Thm.instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
in
cut_tac norm_eq_th i
THEN (simp_tac cring_ctxt i)
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Jul 27 17:44:55 2015 +0200
@@ -87,23 +87,23 @@
val q = Thm.rhs_of nth
val qx = Thm.rhs_of nthx
val enth = Drule.arg_cong_rule ce nthx
- val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
+ val [th0,th1] = map (Thm.instantiate' [SOME cT] []) @{thms "finite.intros"}
fun ins x th =
- Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
+ Thm.implies_elim (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
(Thm.cprop_of th), SOME x] th1) th
val fU = fold ins u th0
val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU)
local
- val insI1 = instantiate' [SOME cT] [] @{thm "insertI1"}
- val insI2 = instantiate' [SOME cT] [] @{thm "insertI2"}
+ val insI1 = Thm.instantiate' [SOME cT] [] @{thm "insertI1"}
+ val insI2 = Thm.instantiate' [SOME cT] [] @{thm "insertI2"}
in
fun provein x S =
case Thm.term_of S of
Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S])
| Const(@{const_name insert}, _) $ y $_ =>
let val (cy,S') = Thm.dest_binop S
- in if Thm.term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
- else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
+ in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1
+ else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2)
(provein x S')
end
end
@@ -141,11 +141,11 @@
else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
else raise Fail "decomp_mpinf: Impossible case!!") fm
val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
- if c = Nox then map (instantiate' [] [SOME fm])
+ if c = Nox then map (Thm.instantiate' [] [SOME fm])
[minf_P, pinf_P, nmi_P, npi_P, ld_P]
else
let val [mi_th,pi_th,nmi_th,npi_th,ld_th] =
- map (instantiate' [] [SOME t])
+ map (Thm.instantiate' [] [SOME t])
(case c of Lt => [minf_lt, pinf_lt, nmi_lt, npi_lt, ld_lt]
| Le => [minf_le, pinf_le, nmi_le, npi_le, ld_le]
| Gt => [minf_gt, pinf_gt, nmi_gt, npi_gt, ld_gt]
@@ -160,7 +160,7 @@
val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q
val qe_th = Drule.implies_elim_list
((fconv_rule (Thm.beta_conversion true))
- (instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
+ (Thm.instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
qe))
[fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
val bex_conv =
--- a/src/HOL/Decision_Procs/langford.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Mon Jul 27 17:44:55 2015 +0200
@@ -21,10 +21,10 @@
fun prove_finite cT u =
let
- val [th0, th1] = map (instantiate' [SOME cT] []) @{thms finite.intros}
+ val [th0, th1] = map (Thm.instantiate' [SOME cT] []) @{thms finite.intros}
fun ins x th =
Thm.implies_elim
- (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
+ (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
in fold ins u th0 end;
fun simp_rule ctxt =
@@ -39,7 +39,7 @@
val p = Thm.dest_arg ep
val ths =
simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
- (instantiate' [] [SOME p] stupid)
+ (Thm.instantiate' [] [SOME p] stupid)
val (L, U) =
let val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end
@@ -47,7 +47,7 @@
let
val (a, A) = Thm.dest_comb S |>> Thm.dest_arg
val cT = Thm.ctyp_of_cterm a
- val ne = instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
+ val ne = Thm.instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
val f = prove_finite cT (dest_set S)
in (ne, f) end
@@ -114,7 +114,7 @@
val rr = Thm.dest_arg r
val thl = prove_conj tabl (conjuncts rr) |> Drule.implies_intr_hyps
val thr = prove_conj tabr (conjuncts ll) |> Drule.implies_intr_hyps
- val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
+ val eqI = Thm.instantiate' [] [SOME ll, SOME rr] @{thm iffI}
in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
fun contains x ct =
@@ -230,7 +230,7 @@
fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
let
- fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
+ fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"}
fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
val p' = fold_rev gen ts p
--- a/src/HOL/HOLCF/Cfun.thy Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Mon Jul 27 17:44:55 2015 +0200
@@ -145,7 +145,7 @@
val dest = Thm.dest_comb;
val f = (snd o dest o snd o dest) ct;
val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
- val tr = instantiate' [SOME T, SOME U] [SOME f]
+ val tr = Thm.instantiate' [SOME T, SOME U] [SOME f]
(mk_meta_eq @{thm Abs_cfun_inverse2});
val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Mon Jul 27 17:44:55 2015 +0200
@@ -213,7 +213,7 @@
val (n2, t2) = cons2typ n1 cons
in (n2, mk_ssumT (t1, t2)) end
val ct = Thm.global_ctyp_of thy (snd (cons2typ 1 spec'))
- val thm1 = instantiate' [SOME ct] [] @{thm exh_start}
+ val thm1 = Thm.instantiate' [SOME ct] [] @{thm exh_start}
val thm2 = rewrite_rule (Proof_Context.init_global thy)
(map mk_meta_eq @{thms ex_bottom_iffs}) thm1
val thm3 = rewrite_rule (Proof_Context.init_global thy)
--- a/src/HOL/HOLCF/Tools/cont_proc.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML Mon Jul 27 17:44:55 2015 +0200
@@ -121,7 +121,7 @@
local
fun solve_cont ctxt t =
let
- val tr = instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
+ val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end
in
fun cont_proc thy =
--- a/src/HOL/HOLCF/Tools/fixrec.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Mon Jul 27 17:44:55 2015 +0200
@@ -153,7 +153,7 @@
val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT)
val predicate = lambda_tuple lhss (list_comb (P, lhss))
val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
- |> Drule.instantiate' [] [SOME (Thm.global_cterm_of thy predicate)]
+ |> Thm.instantiate' [] [SOME (Thm.global_cterm_of thy predicate)]
|> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict}
val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
|> Local_Defs.unfold lthy @{thms split_conv}
--- a/src/HOL/Import/import_rule.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Import/import_rule.ML Mon Jul 27 17:44:55 2015 +0200
@@ -55,7 +55,7 @@
let
val (tml, tmr) = Thm.dest_binop (strip_imp_concl (Thm.cprop_of th))
val cty = Thm.ctyp_of_cterm tml
- val i = Drule.instantiate' [SOME cty] [SOME tml, SOME tmr]
+ val i = Thm.instantiate' [SOME cty] [SOME tml, SOME tmr]
@{thm meta_eq_to_obj_eq}
in
Thm.implies_elim i th
@@ -66,7 +66,7 @@
fun eq_mp th1 th2 =
let
val (tm1l, tm1r) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th1)))
- val i1 = Drule.instantiate' [] [SOME tm1l, SOME tm1r] @{thm iffD1}
+ val i1 = Thm.instantiate' [] [SOME tm1l, SOME tm1r] @{thm iffD1}
val i2 = meta_mp i1 th1
in
meta_mp i2 th2
@@ -79,7 +79,7 @@
val (cf, cg) = Thm.dest_binop t1c
val (cx, cy) = Thm.dest_binop t2c
val [fd, fr] = Thm.dest_ctyp (Thm.ctyp_of_cterm cf)
- val i1 = Drule.instantiate' [SOME fd, SOME fr]
+ val i1 = Thm.instantiate' [SOME fd, SOME fr]
[SOME cf, SOME cg, SOME cx, SOME cy] @{thm cong}
val i2 = meta_mp i1 th1
in
@@ -93,7 +93,7 @@
val (r, s) = Thm.dest_binop t1c
val (_, t) = Thm.dest_binop t2c
val ty = Thm.ctyp_of_cterm r
- val i1 = Drule.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
+ val i1 = Thm.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
val i2 = meta_mp i1 th1
in
meta_mp i2 th2
@@ -107,7 +107,7 @@
val th2a = implies_elim_all th2
val th1b = Thm.implies_intr th2c th1a
val th2b = Thm.implies_intr th1c th2a
- val i = Drule.instantiate' []
+ val i = Thm.instantiate' []
[SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
val i1 = Thm.implies_elim i (Thm.assume (Thm.cprop_of th2b))
val i2 = Thm.implies_elim i1 th1b
@@ -120,7 +120,7 @@
fun conj1 th =
let
val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
- val i = Drule.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct1}
+ val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct1}
in
meta_mp i th
end
@@ -128,7 +128,7 @@
fun conj2 th =
let
val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (Thm.cprop_of th)))
- val i = Drule.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct2}
+ val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct2}
in
meta_mp i th
end
@@ -137,7 +137,7 @@
let
val cty = Thm.ctyp_of_cterm ctm
in
- Drule.instantiate' [SOME cty] [SOME ctm] @{thm refl}
+ Thm.instantiate' [SOME cty] [SOME ctm] @{thm refl}
end
fun abs cv th =
@@ -151,7 +151,7 @@
val th2 = trans (trans bl th1) br
val th3 = implies_elim_all th2
val th4 = Thm.forall_intr cv th3
- val i = Drule.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)]
+ val i = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)]
[SOME ll, SOME lr] @{thm ext2}
in
meta_mp i th4
@@ -202,7 +202,7 @@
val P = Thm.dest_arg cn
val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
in
- Drule.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
+ Thm.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
SOME (Thm.global_cterm_of thy (Free ("a", Thm.typ_of nty))),
SOME (Thm.global_cterm_of thy (Free ("r", Thm.typ_of oty)))] @{thm typedef_hol2hollight}
end
@@ -210,7 +210,7 @@
fun tydef' tycname abs_name rep_name cP ct td_th thy =
let
val ctT = Thm.ctyp_of_cterm ct
- val nonempty = Drule.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
+ val nonempty = Thm.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
val th2 = meta_mp nonempty td_th
val c =
case Thm.concl_of th2 of
@@ -228,7 +228,7 @@
val rept = Thm.dest_arg th_s
val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
val typedef_th =
- Drule.instantiate'
+ Thm.instantiate'
[SOME nty, SOME oty]
[SOME rept, SOME abst, SOME cP, SOME (Thm.global_cterm_of thy' (Free ("a", aty))),
SOME (Thm.global_cterm_of thy' (Free ("r", Thm.typ_of ctT)))]
--- a/src/HOL/Library/Code_Abstract_Nat.thy Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Mon Jul 27 17:44:55 2015 +0200
@@ -77,7 +77,7 @@
val thm' =
Thm.implies_elim
(Conv.fconv_rule (Thm.beta_conversion true)
- (Drule.instantiate'
+ (Thm.instantiate'
[SOME (Thm.ctyp_of_cterm ct)] [SOME (Thm.lambda cv ct),
SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv']
Suc_if_eq)) (Thm.forall_intr cv' thm)
--- a/src/HOL/Library/Countable.thy Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Library/Countable.thy Mon Jul 27 17:44:55 2015 +0200
@@ -182,7 +182,7 @@
val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
val insts = vars |> map (fn (_, T) => try (Thm.cterm_of ctxt)
(Const (@{const_name Countable.finite_item}, T)))
- val induct_thm' = Drule.instantiate' [] insts induct_thm
+ val induct_thm' = Thm.instantiate' [] insts induct_thm
val rules = @{thms finite_item.intros}
in
SOLVED' (fn i => EVERY
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon Jul 27 17:44:55 2015 +0200
@@ -1047,7 +1047,7 @@
ctxt addsimps @{thms field_simps}
addsimps [@{thm nonzero_power_divide}, @{thm power_divide}]
val th =
- instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
+ Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
(if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
else @{lemma "(d=0 --> P) & (d ~= (0::real) --> P) ==> P" by blast})
in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
--- a/src/HOL/Library/positivstellensatz.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Mon Jul 27 17:44:55 2015 +0200
@@ -317,7 +317,7 @@
| _ => raise CTERM ("find_cterm",[t]);
(* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
-fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
+fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
@@ -396,9 +396,9 @@
fun add_rule th th' = fconv_rule (arg_conv (oprconv poly_add_conv))
(match_mp_rule pth_add [th, th'])
fun emul_rule ct th = fconv_rule (arg_conv (oprconv poly_mul_conv))
- (instantiate' [] [SOME ct] (th RS pth_emul))
+ (Thm.instantiate' [] [SOME ct] (th RS pth_emul))
fun square_rule t = fconv_rule (arg_conv (oprconv poly_conv))
- (instantiate' [] [SOME t] pth_square)
+ (Thm.instantiate' [] [SOME t] pth_square)
fun hol_of_positivstellensatz(eqs,les,lts) proof =
let
@@ -444,7 +444,7 @@
if c aconvc (concl th2) then ()
else error "disj_cases : conclusions not alpha convertible"
in Thm.implies_elim (Thm.implies_elim
- (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
+ (Thm.implies_elim (Thm.instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
(Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
(Thm.implies_intr (Thm.apply @{cterm Trueprop} q) th2)
end
@@ -518,9 +518,9 @@
(instantiate_cterm' [SOME (Thm.ctyp_of_cterm x)] [] @{cpat "All :: (?'a => bool) => _" })
(Thm.abstract_rule (name_of x) x th)
- val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
+ val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
- fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
+ fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
fun choose v th th' =
@@ -530,7 +530,7 @@
val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
val th0 = fconv_rule (Thm.beta_conversion true)
- (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
+ (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
val pv = (Thm.rhs_of o Thm.beta_conversion true)
(Thm.apply @{cterm Trueprop} (Thm.apply p v))
val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
@@ -579,7 +579,7 @@
(prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
end
- in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
+ in (Thm.implies_elim (Thm.instantiate' [] [SOME ct] pth_final) th, certificates)
end
in f
end;
@@ -710,7 +710,7 @@
(eq_pols @ le_pols @ lt_pols) [])
val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
- val le' = le @ map (fn a => instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens
+ val le' = le @ map (fn a => Thm.instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens
in ((translator (eq,le',lt) proof), Trivial)
end
end;
@@ -725,9 +725,9 @@
val absmaxmin_elim_conv2 =
let
- val pth_abs = instantiate' [SOME @{ctyp real}] [] abs_split'
- val pth_max = instantiate' [SOME @{ctyp real}] [] max_split
- val pth_min = instantiate' [SOME @{ctyp real}] [] min_split
+ val pth_abs = Thm.instantiate' [SOME @{ctyp real}] [] abs_split'
+ val pth_max = Thm.instantiate' [SOME @{ctyp real}] [] max_split
+ val pth_min = Thm.instantiate' [SOME @{ctyp real}] [] min_split
val abs_tm = @{cterm "abs :: real => _"}
val p_v = (("P", 0), @{typ "real \<Rightarrow> bool"})
val x_v = (("x", 0), @{typ real})
--- a/src/HOL/Multivariate_Analysis/normarith.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Mon Jul 27 17:44:55 2015 +0200
@@ -154,7 +154,7 @@
(Numeral.mk_cnumber @{ctyp "real"} b)
end;
-fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
+fun norm_cmul_rule c th = Thm.instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm};
@@ -342,7 +342,7 @@
val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) []
val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
- fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
+ fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm l)] [] @{cpat "op == :: ?'a =>_"}) l) r
val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Thm.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns
--- a/src/HOL/Nominal/nominal_datatype.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Jul 27 17:44:55 2015 +0200
@@ -110,7 +110,7 @@
val dj_cp' = [cp, dj] MRS dj_cp;
val cert = SOME o Thm.cterm_of ctxt
in
- SOME (mk_meta_eq (Drule.instantiate' [SOME (Thm.ctyp_of ctxt S)]
+ SOME (mk_meta_eq (Thm.instantiate' [SOME (Thm.ctyp_of ctxt S)]
[cert t, cert r, cert s] dj_cp'))
end
else NONE
@@ -1282,7 +1282,7 @@
_ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ _)) $ _ => U = T
| _ => false)) perm_fresh_fresh
in
- Drule.instantiate' []
+ Thm.instantiate' []
[SOME (Thm.global_cterm_of thy a), NONE, SOME (Thm.global_cterm_of thy b)] th
end;
--- a/src/HOL/Nominal/nominal_inductive.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Jul 27 17:44:55 2015 +0200
@@ -203,7 +203,7 @@
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
- val inductive_forall_def' = Drule.instantiate'
+ val inductive_forall_def' = Thm.instantiate'
[SOME (Thm.global_ctyp_of thy fsT)] [] inductive_forall_def;
fun lift_pred' t (Free (s, T)) ts =
@@ -488,7 +488,7 @@
let
val (cf, ct) =
Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th));
- val arg_cong' = Drule.instantiate'
+ val arg_cong' = Thm.instantiate'
[SOME (Thm.ctyp_of_cterm ct)]
[NONE, SOME ct, SOME cf] (arg_cong RS iffD2);
val inst = Thm.first_order_match (ct,
--- a/src/HOL/Nominal/nominal_inductive2.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Jul 27 17:44:55 2015 +0200
@@ -227,7 +227,7 @@
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
- val inductive_forall_def' = Drule.instantiate'
+ val inductive_forall_def' = Thm.instantiate'
[SOME (Thm.global_ctyp_of thy fsT)] [] inductive_forall_def;
fun lift_pred' t (Free (s, T)) ts =
@@ -316,7 +316,7 @@
val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
val fs_atom = Global_Theory.get_thm thy
("fs_" ^ Long_Name.base_name atom ^ "1");
- val avoid_th = Drule.instantiate'
+ val avoid_th = Thm.instantiate'
[SOME (Thm.global_ctyp_of thy (fastype_of p))] [SOME (Thm.global_cterm_of thy p)]
([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
val (([(_, cx)], th1 :: th2 :: ths), ctxt') = Obtain.result
--- a/src/HOL/Nominal/nominal_permeq.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Mon Jul 27 17:44:55 2015 +0200
@@ -197,13 +197,13 @@
in
if pi1 <> pi2 then (* only apply the composition rule in this case *)
if T = U then
- SOME (Drule.instantiate'
+ SOME (Thm.instantiate'
[SOME (Thm.global_ctyp_of thy (fastype_of t))]
[SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
(mk_meta_eq ([Global_Theory.get_thm thy ("pt_"^tname'^"_inst"),
Global_Theory.get_thm thy ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
else
- SOME (Drule.instantiate'
+ SOME (Thm.instantiate'
[SOME (Thm.global_ctyp_of thy (fastype_of t))]
[SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
(mk_meta_eq (Global_Theory.get_thm thy ("cp_"^tname'^"_"^uname'^"_inst") RS
--- a/src/HOL/Probability/measurable.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Probability/measurable.ML Mon Jul 27 17:44:55 2015 +0200
@@ -252,7 +252,7 @@
val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
fun inst (ts, Ts) =
- Drule.instantiate' (cert Thm.global_ctyp_of Ts) (cert Thm.global_cterm_of ts)
+ Thm.instantiate' (cert Thm.global_ctyp_of Ts) (cert Thm.global_cterm_of ts)
@{thm measurable_compose_countable}
in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end
handle TERM _ => no_tac) 1)
--- a/src/HOL/String.thy Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/String.thy Mon Jul 27 17:44:55 2015 +0200
@@ -253,7 +253,7 @@
put_simpset HOL_ss @{context}
addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
fun mk_code_eqn x y =
- Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
+ Thm.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
|> simplify simpset;
val code_eqns = map_product mk_code_eqn nibbles nibbles;
in
--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Jul 27 17:44:55 2015 +0200
@@ -1251,7 +1251,7 @@
map Bound (live - 1 downto 0)) $ Bound live));
val cts = [NONE, SOME (Thm.cterm_of lthy tinst)];
in
- Drule.instantiate' cTs cts @{thm surj_imp_ordLeq}
+ Thm.instantiate' cTs cts @{thm surj_imp_ordLeq}
end);
val bd = mk_cexp
(if live = 0 then ctwo
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jul 27 17:44:55 2015 +0200
@@ -1838,7 +1838,7 @@
val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
- fun mk_case_split' cp = Drule.instantiate' [] [SOME (Thm.cterm_of lthy cp)] @{thm case_split};
+ fun mk_case_split' cp = Thm.instantiate' [] [SOME (Thm.cterm_of lthy cp)] @{thm case_split};
val case_splitss' = map (map mk_case_split') cpss;
@@ -1864,7 +1864,7 @@
let
val (domT, ranT) = dest_funT (fastype_of sel);
val arg_cong' =
- Drule.instantiate' (map (SOME o Thm.ctyp_of lthy) [domT, ranT])
+ Thm.instantiate' (map (SOME o Thm.ctyp_of lthy) [domT, ranT])
[NONE, NONE, SOME (Thm.cterm_of lthy sel)] arg_cong
|> Thm.varifyT_global;
val sel_thm' = sel_thm RSN (2, trans);
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Jul 27 17:44:55 2015 +0200
@@ -142,7 +142,7 @@
fun mk_ctor_iff_dtor_tac ctxt cTs cctor cdtor ctor_dtor dtor_ctor =
HEADGOAL (rtac ctxt iffI THEN'
EVERY' (@{map 3} (fn cTs => fn cx => fn th =>
- dtac ctxt (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
+ dtac ctxt (Thm.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN'
assume_tac ctxt) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor]));
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jul 27 17:44:55 2015 +0200
@@ -497,7 +497,7 @@
val T = mk_tupleT_balanced tfrees;
in
@{thm asm_rl[of "ALL x. P x --> Q x" for P Q]}
- |> Drule.instantiate' [SOME (Thm.ctyp_of @{context} T)] []
+ |> Thm.instantiate' [SOME (Thm.ctyp_of @{context} T)] []
|> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]}
|> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
|> Thm.varifyT_global
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Jul 27 17:44:55 2015 +0200
@@ -1975,7 +1975,7 @@
in
@{map 6} (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
((set_minimal
- |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y')
+ |> Thm.instantiate' cTs (mk_induct_tinst phis jsets y y')
|> unfold_thms lthy incls) OF
(replicate n ballI @
maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
@@ -2107,7 +2107,7 @@
val cphis = @{map 9} mk_cphi
Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
- val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
+ val coinduct = Thm.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Mon Jul 27 17:44:55 2015 +0200
@@ -157,7 +157,7 @@
let
val s = Name.uu;
val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
- val split' = Drule.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split;
+ val split' = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split;
in
Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
end
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Jul 27 17:44:55 2015 +0200
@@ -175,7 +175,7 @@
rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1;
fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs =
- EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
+ EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn thm => EVERY'
[rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm empty_subsetI}]) rec_0s,
@@ -195,7 +195,7 @@
REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], assume_tac ctxt])) (1 upto n)) 1
fun mk_mor_col_tac ctxt m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss =
- EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
+ EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn thm => EVERY' (map (rtac ctxt) [impI, thm RS trans, thm RS sym])) rec_0s,
REPEAT_DETERM o rtac ctxt allI,
@@ -400,7 +400,7 @@
val n = length Lev_0s;
val ks = n downto 1;
in
- EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
+ EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn Lev_0 =>
EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
@@ -425,7 +425,7 @@
val n = length rv_Nils;
val ks = 1 upto n;
in
- EVERY' [rtac ctxt (Drule.instantiate' cTs cts @{thm list.induct}),
+ EVERY' [rtac ctxt (Thm.instantiate' cTs cts @{thm list.induct}),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn rv_Cons =>
CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac ctxt exI,
@@ -450,7 +450,7 @@
val n = length Lev_0s;
val ks = 1 upto n;
in
- EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
+ EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
@@ -496,7 +496,7 @@
val n = length Lev_0s;
val ks = 1 upto n;
in
- EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
+ EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
@@ -867,7 +867,7 @@
let
val n = length dtor_maps;
in
- EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
+ EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac ctxt allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
CONJ_WRAP' (K (rtac ctxt @{thm image_empty})) rec_0s,
REPEAT_DETERM o rtac ctxt allI,
@@ -889,7 +889,7 @@
let
val n = length rec_0s;
in
- EVERY' [rtac ctxt (Drule.instantiate' [] cts nat_induct),
+ EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac ctxt allI,
CONJ_WRAP' (fn rec_0 => EVERY' (map (rtac ctxt) [ordIso_ordLeq_trans,
@{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s,
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Jul 27 17:44:55 2015 +0200
@@ -1581,7 +1581,7 @@
(@{map 4} (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
val inducts = map (fn cphis =>
- Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
+ Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
val goals =
@{map 3} (fn f => fn sets => fn sets' =>
@@ -1610,7 +1610,7 @@
val cphiss = map (map2 mk_cphi Izs) Isetss_by_range;
val inducts = map (fn cphis =>
- Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
+ Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
val goals =
map (fn sets =>
@@ -1645,7 +1645,7 @@
val cphis = @{map 4} mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
- val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
+ val induct = Thm.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
val goal =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -1706,7 +1706,7 @@
val cxs = map (SOME o Thm.cterm_of lthy) (splice Izs1 Izs2);
fun mk_cphi z1 z2 goal = SOME (Thm.cterm_of lthy (Term.absfree z1 (Term.absfree z2 goal)));
val cphis = @{map 3} mk_cphi Izs1' Izs2' goals;
- val induct = Drule.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
+ val induct = Thm.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
in
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Jul 27 17:44:55 2015 +0200
@@ -222,7 +222,7 @@
suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite =
let
val induct = worel RS
- Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
+ Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
val src = 1 upto m + 1;
val dest = (m + 1) :: (1 upto m);
val absorbAs_tac = if m = 0 then K (all_tac)
@@ -268,7 +268,7 @@
fun mk_min_algs_least_tac ctxt cT ct worel min_algs alg_sets =
let
val induct = worel RS
- Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
+ Thm.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};
val minG_tac =
EVERY' [rtac ctxt @{thm UN_least}, etac ctxt allE, dtac ctxt mp, etac ctxt @{thm underS_E},
@@ -444,7 +444,7 @@
fun mk_mor_fold_tac ctxt cT ct fold_defs ex_mor mor =
(EVERY' (map (stac ctxt) fold_defs) THEN' EVERY' [rtac ctxt rev_mp, rtac ctxt ex_mor, rtac ctxt impI] THEN'
REPEAT_DETERM_N (length fold_defs) o etac ctxt exE THEN'
- rtac ctxt (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1;
+ rtac ctxt (Thm.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1;
fun mk_fold_unique_mor_tac ctxt type_defs init_unique_mors Reps mor_comp mor_Abs mor_fold =
let
@@ -515,7 +515,7 @@
assume_tac ctxt],
assume_tac ctxt];
in
- EVERY' [rtac ctxt rev_mp, rtac ctxt (Drule.instantiate' cTs cts ctor_induct),
+ EVERY' [rtac ctxt rev_mp, rtac ctxt (Thm.instantiate' cTs cts ctor_induct),
EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac ctxt impI,
REPEAT_DETERM o eresolve_tac ctxt [conjE, allE],
CONJ_WRAP' (K (assume_tac ctxt)) ks] 1
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jul 27 17:44:55 2015 +0200
@@ -690,7 +690,7 @@
(map Logic.varifyT_global As ~~ As);
fun inst_thm t thm =
- Drule.instantiate' [] [SOME (Thm.cterm_of lthy t)]
+ Thm.instantiate' [] [SOME (Thm.cterm_of lthy t)]
(Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm));
val uexhaust_thm = inst_thm u exhaust_thm;
--- a/src/HOL/Tools/Function/function_context_tree.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Function/function_context_tree.ML Mon Jul 27 17:44:55 2015 +0200
@@ -248,7 +248,7 @@
val iha = import_thm ctxt (fix, h_as) ha (* (a', h a') : G *)
|> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
(* (a, h a) : G *)
- val inst_ih = instantiate' [] [SOME (Thm.cterm_of ctxt arg)] ih
+ val inst_ih = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt arg)] ih
val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
val h_a'_eq_h_a = Thm.combination (Thm.reflexive (Thm.cterm_of ctxt h)) inner
--- a/src/HOL/Tools/Function/function_core.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Mon Jul 27 17:44:55 2015 +0200
@@ -371,7 +371,7 @@
val exactly_one =
@{thm ex1I}
- |> instantiate'
+ |> Thm.instantiate'
[SOME (Thm.ctyp_of ctxt ranT)]
[SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
|> curry (op COMP) existence
@@ -407,7 +407,7 @@
val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
- |> instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
+ |> Thm.instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
val _ = trace_msg (K "Proving Replacement lemmas...")
val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses
@@ -694,7 +694,7 @@
|> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
|> assume_tac ctxt 1 |> Seq.hd
|> (curry op COMP) (acc_downward
- |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
+ |> (Thm.instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
|> Thm.forall_intr (Thm.cterm_of ctxt z)
|> Thm.forall_intr (Thm.cterm_of ctxt x))
|> Thm.forall_intr (Thm.cterm_of ctxt a)
--- a/src/HOL/Tools/Function/induction_schema.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Mon Jul 27 17:44:55 2015 +0200
@@ -374,7 +374,7 @@
|> Thm.cterm_of ctxt''
in
indthm
- |> Drule.instantiate' [] [SOME inst]
+ |> Thm.instantiate' [] [SOME inst]
|> simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt'')
|> Conv.fconv_rule (ind_rulify ctxt'')
end
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Jul 27 17:44:55 2015 +0200
@@ -278,7 +278,7 @@
THEN (resolve_tac ctxt @{thms reduction_pair_lemma} 1)
THEN (resolve_tac ctxt @{thms rp_inv_image_rp} 1)
THEN (resolve_tac ctxt [order_rpair ms_rp label] 1)
- THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
+ THEN PRIMITIVE (Thm.instantiate' [] [SOME level_mapping])
THEN unfold_tac ctxt @{thms rp_inv_image_def}
THEN Local_Defs.unfold_tac ctxt @{thms split_conv fst_conv snd_conv}
THEN REPEAT (SOMEGOAL (resolve_tac ctxt [@{thm Un_least}, @{thm empty_subsetI}]))
--- a/src/HOL/Tools/Lifting/lifting_term.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Mon Jul 27 17:44:55 2015 +0200
@@ -409,7 +409,7 @@
then
let
val instantiated_id_quot_thm =
- instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
+ Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
in
(instantiated_id_quot_thm, (table, ctxt))
end
--- a/src/HOL/Tools/Meson/meson.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Mon Jul 27 17:44:55 2015 +0200
@@ -173,7 +173,7 @@
let
val cc = Thm.cterm_of ctxt c
val ct = Thm.dest_arg (Thm.cprop_of th)
- in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
+ in resolve_tac ctxt [th] i (Thm.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
| _ => resolve_tac ctxt [th] i st
(*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
--- a/src/HOL/Tools/Meson/meson_clausify.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Jul 27 17:44:55 2015 +0200
@@ -102,13 +102,13 @@
val cxT = Thm.ctyp_of ctxt xT
val cbodyT = Thm.ctyp_of ctxt bodyT
fun makeK () =
- instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.cterm_of ctxt body)] @{thm abs_K}
+ Thm.instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.cterm_of ctxt body)] @{thm abs_K}
in
case body of
Const _ => makeK()
| Free _ => makeK()
| Var _ => makeK() (*though Var isn't expected*)
- | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
+ | Bound 0 => Thm.instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
| rator$rand =>
if Term.is_dependent rator then (*C or S*)
if Term.is_dependent rand then (*S*)
--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Jul 27 17:44:55 2015 +0200
@@ -50,7 +50,7 @@
let
val ct = Thm.cterm_of ctxt t
val cT = Thm.ctyp_of_cterm ct
- in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
+ in refl |> Thm.instantiate' [SOME cT] [SOME ct] end
| Const (@{const_name disj}, _) $ t1 $ t2 =>
(if can HOLogic.dest_not t1 then t2 else t1)
|> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Jul 27 17:44:55 2015 +0200
@@ -397,7 +397,7 @@
(* prove inj Rep_dt_i and Rep_dt_i x : rep_set_dt_i *)
val fun_congs =
- map (fn T => make_elim (Drule.instantiate' [SOME (Thm.global_ctyp_of thy5 T)] [] fun_cong)) branchTs;
+ map (fn T => make_elim (Thm.instantiate' [SOME (Thm.global_ctyp_of thy5 T)] [] fun_cong)) branchTs;
fun prove_iso_thms ds (inj_thms, elem_thms) =
let
--- a/src/HOL/Tools/Qelim/cooper.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon Jul 27 17:44:55 2015 +0200
@@ -84,17 +84,17 @@
val is_number = can dest_number;
val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
- map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
+ map (Thm.instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =
- map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
+ map (Thm.instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] =
- map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
+ map (Thm.instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
-val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
+val [miP, piP] = map (Thm.instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
-val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
+val infDP = Thm.instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,
asetgt, asetge, asetdvd, asetndvd,asetP],
@@ -103,7 +103,7 @@
val [cpmi, cppi] = [@{thm "cpmi"}, @{thm "cppi"}];
-val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
+val unity_coeff_ex = Thm.instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
val [zdvd_mono,simp_from_to,all_not_ex] =
[@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
@@ -166,9 +166,9 @@
in (mi_th, set_th, infD_th)
end;
-val inst' = fn cts => instantiate' [] (map SOME cts);
-val infDTrue = instantiate' [] [SOME true_tm] infDP;
-val infDFalse = instantiate' [] [SOME false_tm] infDP;
+val inst' = fn cts => Thm.instantiate' [] (map SOME cts);
+val infDTrue = Thm.instantiate' [] [SOME true_tm] infDP;
+val infDFalse = Thm.instantiate' [] [SOME false_tm] infDP;
val cadd = @{cterm "op + :: int => _"}
val cmulC = @{cterm "op * :: int => _"}
@@ -483,16 +483,16 @@
in Thm.equal_elim (Thm.symmetric th) TrueI end;
(* A and B set *)
local
- val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
- val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
+ val insI1 = Thm.instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
+ val insI2 = Thm.instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
in
fun provein x S =
case Thm.term_of S of
Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
| Const(@{const_name insert}, _) $ y $ _ =>
let val (cy,S') = Thm.dest_binop S
- in if Thm.term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
- else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
+ in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1
+ else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2)
(provein x S')
end
end
@@ -519,7 +519,7 @@
let
val sths = map (fn (tl,t0) =>
if tl = Thm.term_of t0
- then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
+ then Thm.instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
else provelin ctxt ((HOLogic.eq_const iT)$tl$(Thm.term_of t0)
|> HOLogic.mk_Trueprop))
(sl ~~ s0)
@@ -527,7 +527,7 @@
val S = mkISet csl
val inStab = fold (fn ct => fn tab => Termtab.update (Thm.term_of ct, provein ct S) tab)
csl Termtab.empty
- val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
+ val eqelem_th = Thm.instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
val inS =
let
val tab = fold Termtab.update
@@ -536,7 +536,7 @@
val th =
if s aconvc t
then the (Termtab.lookup inStab (Thm.term_of s))
- else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
+ else FWD (Thm.instantiate' [] [SOME s, SOME t] eqelem_th)
[eq, the (Termtab.lookup inStab (Thm.term_of s))]
in (Thm.term_of t, th) end) sths) Termtab.empty
in
@@ -801,7 +801,7 @@
fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
let
- fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
+ fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"}
fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
val p' = fold_rev gen ts p
--- a/src/HOL/Tools/Qelim/qelim.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Mon Jul 27 17:44:55 2015 +0200
@@ -45,7 +45,7 @@
let
val p = Thm.dest_arg p
val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
- val th = instantiate' [SOME T] [SOME p] all_not_ex
+ val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex
in Thm.transitive th (conv env (Thm.rhs_of th))
end
| _ => atcv env p
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Jul 27 17:44:55 2015 +0200
@@ -80,7 +80,7 @@
val cty = Thm.global_ctyp_of thy ty;
in
@{thm partial_term_of_anything}
- |> Drule.instantiate' [SOME cty] insts
+ |> Thm.instantiate' [SOME cty] insts
|> Thm.varifyT_global
end
@@ -99,7 +99,7 @@
@{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
val var_eq =
@{thm partial_term_of_anything}
- |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
+ |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
|> Thm.varifyT_global
val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs;
in
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Jul 27 17:44:55 2015 +0200
@@ -99,7 +99,7 @@
val ty_inst = map (SOME o Thm.ctyp_of ctxt) [domain_type (fastype_of R2)]
val trm_inst = map (SOME o Thm.cterm_of ctxt) [R2, R1]
in
- (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
+ (case try (Thm.instantiate' ty_inst trm_inst) ball_bex_thm of
NONE => NONE
| SOME thm' =>
(case try (get_match_inst thy (get_lhs thm')) redex of
@@ -198,7 +198,7 @@
val cfx = Thm.cterm_of ctxt fx;
val cxt = Thm.ctyp_of ctxt (fastype_of x);
val cfxt = Thm.ctyp_of ctxt (fastype_of fx);
- val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
+ val thm = Thm.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
in
Conv.rewr_conv thm ctrm
end)
@@ -247,7 +247,7 @@
val ty_f = range_type (fastype_of f)
val ty_inst = map (SOME o Thm.ctyp_of ctxt) [ty_x, ty_b, ty_f]
val t_inst = map (SOME o Thm.cterm_of ctxt) [R2, f, g, x, y];
- val inst_thm = Drule.instantiate' ty_inst
+ val inst_thm = Thm.instantiate' ty_inst
([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
in
(resolve_tac ctxt [inst_thm] THEN' SOLVED' (quotient_tac ctxt)) 1
@@ -264,7 +264,7 @@
let
val ty = domain_type (fastype_of R)
in
- case try (Drule.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
+ case try (Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
[SOME (Thm.cterm_of ctxt R)]) @{thm equals_rsp} of
SOME thm => resolve_tac ctxt [thm] THEN' quotient_tac ctxt
| NONE => K no_tac
@@ -281,7 +281,7 @@
in
case try (map (SOME o Thm.cterm_of ctxt)) [rel, abs, rep] of
SOME t_inst =>
- (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
+ (case try (Thm.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
SOME inst_thm => (resolve_tac ctxt [inst_thm] THEN' quotient_tac ctxt) i
| NONE => no_tac)
| NONE => no_tac
@@ -468,7 +468,7 @@
val (ty_c, ty_d) = dest_funT (fastype_of a2)
val tyinst = map (SOME o Thm.ctyp_of ctxt) [ty_a, ty_b, ty_c, ty_d]
val tinst = [NONE, NONE, SOME (Thm.cterm_of ctxt r1), NONE, SOME (Thm.cterm_of ctxt a2)]
- val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
+ val thm1 = Thm.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
val (insp, inst) =
@@ -529,7 +529,7 @@
(* Tactic for Generalising Free Variables in a Goal *)
fun inst_spec ctrm =
- Drule.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec}
+ Thm.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec}
fun inst_spec_tac ctxt ctrms =
EVERY' (map (dresolve_tac ctxt o single o inst_spec) ctrms)
@@ -602,7 +602,7 @@
val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
- Drule.instantiate' []
+ Thm.instantiate' []
[SOME (Thm.cterm_of ctxt rtrm'),
SOME (Thm.cterm_of ctxt reg_goal),
NONE,
@@ -661,7 +661,7 @@
val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
- Drule.instantiate' []
+ Thm.instantiate' []
[SOME (Thm.cterm_of ctxt reg_goal),
NONE,
SOME (Thm.cterm_of ctxt inj_goal)] partiality_procedure_thm
--- a/src/HOL/Tools/Transfer/transfer.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Mon Jul 27 17:44:55 2015 +0200
@@ -218,7 +218,7 @@
fun Rel_conv ct =
let val (cT, cT') = dest_funcT (Thm.ctyp_of_cterm ct)
val (cU, _) = dest_funcT cT'
- in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
+ in Thm.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
(* Conversion to preprocess a transfer rule *)
fun safe_Rel_conv ct =
@@ -463,7 +463,7 @@
val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
- val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
+ val rule = Thm.instantiate' tinsts insts @{thm Rel_abs}
val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
in
(thm2 COMP rule, hyps)
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Mon Jul 27 17:44:55 2015 +0200
@@ -359,7 +359,7 @@
val kill_True = Local_Defs.unfold lthy [@{thm HOL.simp_thms(21)}]
in
thm
- |> Drule.instantiate' cTs cts
+ |> Thm.instantiate' cTs cts
|> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
(Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
|> Local_Defs.unfold lthy eq_onps
--- a/src/HOL/Tools/choice_specification.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML Mon Jul 27 17:44:55 2015 +0200
@@ -138,7 +138,7 @@
let
val cv = Thm.global_cterm_of thy v
val cT = Thm.ctyp_of_cterm cv
- val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec
+ val spec' = Thm.instantiate' [SOME cT] [NONE, SOME cv] spec
in thm RS spec' end
fun remove_alls frees (thm, thy) = (fold (inst_all thy) frees thm, thy)
fun process_single ((name, atts), rew_imp, frees) args =
--- a/src/HOL/Tools/cnf.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/cnf.ML Mon Jul 27 17:44:55 2015 +0200
@@ -165,7 +165,7 @@
(* ------------------------------------------------------------------------- *)
fun inst_thm thy ts thm =
- instantiate' [] (map (SOME o Thm.global_cterm_of thy) ts) thm;
+ Thm.instantiate' [] (map (SOME o Thm.global_cterm_of thy) ts) thm;
(* ------------------------------------------------------------------------- *)
(* Naive CNF transformation *)
--- a/src/HOL/Tools/code_evaluation.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Mon Jul 27 17:44:55 2015 +0200
@@ -69,7 +69,7 @@
val cty = Thm.global_ctyp_of thy ty;
in
@{thm term_of_anything}
- |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
+ |> Thm.instantiate' [SOME cty] [SOME arg, SOME rhs]
|> Thm.varifyT_global
end;
@@ -106,7 +106,7 @@
val cty = Thm.global_ctyp_of thy ty;
in
@{thm term_of_anything}
- |> Drule.instantiate' [SOME cty] [SOME (Thm.global_cterm_of thy arg), SOME rhs]
+ |> Thm.instantiate' [SOME cty] [SOME (Thm.global_cterm_of thy arg), SOME rhs]
|> Thm.varifyT_global
end;
--- a/src/HOL/Tools/groebner.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/groebner.ML Mon Jul 27 17:44:55 2015 +0200
@@ -413,7 +413,7 @@
fun initial_conv ctxt =
Simplifier.rewrite (put_simpset initial_ss ctxt);
-val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
+val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
val cTrp = @{cterm "Trueprop"};
val cConj = @{cterm HOL.conj};
@@ -435,7 +435,7 @@
fun sym_conv eq =
let val (l,r) = Thm.dest_binop eq
- in instantiate' [SOME (Thm.ctyp_of_cterm l)] [SOME l, SOME r] eq_commute
+ in Thm.instantiate' [SOME (Thm.ctyp_of_cterm l)] [SOME l, SOME r] eq_commute
end;
(* FIXME : copied from cqe.ML -- complex QE*)
@@ -471,14 +471,14 @@
fun tabr c = the (Termtab.lookup ctabr (Thm.term_of c))
val thl = prove_conj tabl (conjuncts r) |> implies_intr_hyps
val thr = prove_conj tabr (conjuncts l) |> implies_intr_hyps
- val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI}
+ val eqI = Thm.instantiate' [] [SOME l, SOME r] @{thm iffI}
in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
(* END FIXME.*)
(* Conversion for the equivalence of existential statements where
EX quantifiers are rearranged differently *)
- fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
+ fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
fun choose v th th' = case Thm.concl_of th of
@@ -487,7 +487,7 @@
val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
val th0 = Conv.fconv_rule (Thm.beta_conversion true)
- (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
+ (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
val pv = (Thm.rhs_of o Thm.beta_conversion true)
(Thm.apply @{cterm Trueprop} (Thm.apply p v))
val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
@@ -504,7 +504,7 @@
val p = Thm.lambda v (Thm.dest_arg (Thm.cprop_of th))
in Thm.implies_elim
(Conv.fconv_rule (Thm.beta_conversion true)
- (instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI}))
+ (Thm.instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI}))
th
end
fun ex_eq_conv t =
@@ -517,7 +517,7 @@
val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th))
val p = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) th1
val q = (Thm.dest_arg o Thm.dest_arg o Thm.cprop_of) th1
- in Thm.implies_elim (Thm.implies_elim (instantiate' [] [SOME p, SOME q] iffI) th1) th2
+ in Thm.implies_elim (Thm.implies_elim (Thm.instantiate' [] [SOME p, SOME q] iffI) th1) th2
|> mk_meta_eq
end;
@@ -739,7 +739,7 @@
let
fun mk_forall x p =
Thm.apply
- (Drule.cterm_rule (instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
+ (Drule.cterm_rule (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
@{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
val avs = Thm.add_cterm_frees tm []
val P' = fold mk_forall avs tm
@@ -775,7 +775,7 @@
fun poly_eq_conv t =
let val (a,b) = Thm.dest_binop t
in Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv ring_normalize_conv))
- (instantiate' [] [SOME a, SOME b] idl_sub)
+ (Thm.instantiate' [] [SOME a, SOME b] idl_sub)
end
val poly_eq_simproc =
let
@@ -810,7 +810,7 @@
| NONE => (the (find_first
(fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th)
val th2 = Thm.transitive th1
- (instantiate' [] [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v]
+ (Thm.instantiate' [] [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v]
idl_add0)
in Conv.fconv_rule(funpow 2 Conv.arg_conv ring_normalize_conv) th2
end
@@ -946,7 +946,7 @@
| _=> raise CTERM ("ideal_tac - lhs",[t])
fun exitac _ NONE = no_tac
| exitac ctxt (SOME y) =
- resolve_tac ctxt [instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1
+ resolve_tac ctxt [Thm.instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1
val claset = claset_of @{context}
in
--- a/src/HOL/Tools/inductive_set.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML Mon Jul 27 17:44:55 2015 +0200
@@ -42,7 +42,7 @@
let
fun close p t f =
let val vs = Term.add_vars t []
- in Drule.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
+ in Thm.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
(p (fold (Logic.all o Var) vs t) f)
end;
fun mkop @{const_name HOL.conj} T x =
--- a/src/HOL/Tools/int_arith.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/int_arith.ML Mon Jul 27 17:44:55 2015 +0200
@@ -27,7 +27,7 @@
fun proc0 phi ctxt ct =
let val T = Thm.ctyp_of_cterm ct
in if Thm.typ_of T = @{typ int} then NONE else
- SOME (instantiate' [SOME T] [] zeroth)
+ SOME (Thm.instantiate' [SOME T] [] zeroth)
end;
val zero_to_of_int_zero_simproc =
@@ -41,7 +41,7 @@
fun proc1 phi ctxt ct =
let val T = Thm.ctyp_of_cterm ct
in if Thm.typ_of T = @{typ int} then NONE else
- SOME (instantiate' [SOME T] [] oneth)
+ SOME (Thm.instantiate' [SOME T] [] oneth)
end;
val one_to_of_int_one_simproc =
--- a/src/HOL/Tools/numeral_simprocs.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon Jul 27 17:44:55 2015 +0200
@@ -610,7 +610,7 @@
val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z,w]
val T = Thm.ctyp_of_cterm x
val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z]
- val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
+ val th = Thm.instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz)
end
handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
@@ -624,13 +624,13 @@
let val (x,y) = Thm.dest_binop l val z = r
val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
val ynz = prove_nz ctxt T y
- in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
+ in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
end
| (_, Const (@{const_name Rings.divide},_)$_$_) =>
let val (x,y) = Thm.dest_binop r val z = l
val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
val ynz = prove_nz ctxt T y
- in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
+ in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
end
| _ => NONE)
end
@@ -648,42 +648,42 @@
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = Thm.ctyp_of_cterm c
- val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
+ val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
in SOME (mk_meta_eq th) end
| Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = Thm.ctyp_of_cterm c
- val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
+ val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
in SOME (mk_meta_eq th) end
| Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = Thm.ctyp_of_cterm c
- val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
+ val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
in SOME (mk_meta_eq th) end
| Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = Thm.ctyp_of_cterm c
- val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
+ val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
in SOME (mk_meta_eq th) end
| Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = Thm.ctyp_of_cterm c
- val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
+ val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
in SOME (mk_meta_eq th) end
| Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = Thm.ctyp_of_cterm c
- val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
+ val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
in SOME (mk_meta_eq th) end
| _ => NONE)
handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
--- a/src/HOL/Tools/record.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/record.ML Mon Jul 27 17:44:55 2015 +0200
@@ -85,7 +85,7 @@
let
val exists_thm =
UNIV_I
- |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type))] [];
+ |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type))] [];
val proj_constr = Abs_inverse OF [exists_thm];
val absT = Type (tyco, map TFree vs);
in
--- a/src/HOL/Tools/semiring_normalizer.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Mon Jul 27 17:44:55 2015 +0200
@@ -142,7 +142,7 @@
let val (a, b) = Rat.quotient_of_rat x
in if b = 1 then Numeral.mk_cnumber cT a
else Thm.apply
- (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
+ (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"})
(Numeral.mk_cnumber cT a))
(Numeral.mk_cnumber cT b)
end
--- a/src/Pure/axclass.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/Pure/axclass.ML Mon Jul 27 17:44:55 2015 +0200
@@ -191,7 +191,7 @@
thy2
|> update_classrel ((c1, c2),
(the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
- |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
+ |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
|> Thm.close_derivation));
val proven = is_classrel thy1;
@@ -234,7 +234,7 @@
let
val th1 =
(th RS the_classrel thy (c, c1))
- |> Drule.instantiate' std_vars []
+ |> Thm.instantiate' std_vars []
|> Thm.close_derivation;
in ((th1, thy_name), c1) end);
@@ -396,7 +396,7 @@
val (th', thy') = Global_Theory.store_thm (binding, th) thy;
val th'' = th'
|> Thm.unconstrainT
- |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
+ |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
in
thy'
|> Sign.primitive_classrel (c1, c2)
@@ -426,7 +426,7 @@
|> (map o apsnd o map_atyps) (K T);
val th'' = th'
|> Thm.unconstrainT
- |> Drule.instantiate' std_vars [];
+ |> Thm.instantiate' std_vars [];
in
thy'
|> fold (#2 oo declare_overloaded) missing_params
--- a/src/Pure/drule.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/Pure/drule.ML Mon Jul 27 17:44:55 2015 +0200
@@ -24,7 +24,6 @@
thm -> thm
val infer_instantiate_types: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm
val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
- val instantiate': ctyp option list -> cterm option list -> thm -> thm
val infer_instantiate': Proof.context -> cterm option list -> thm -> thm
val zero_var_indexes_list: thm list -> thm list
val zero_var_indexes: thm -> thm
@@ -798,26 +797,6 @@
AList.lookup (op =) vars xi |> Option.map (fn T => ((xi, T), cu)));
in infer_instantiate_types ctxt args' th end;
-
-(* instantiate by left-to-right occurrence of variables *)
-
-fun instantiate' cTs cts thm =
- let
- fun err msg =
- raise TYPE ("instantiate': " ^ msg,
- map_filter (Option.map Thm.typ_of) cTs,
- map_filter (Option.map Thm.term_of) cts);
-
- fun zip_vars xs ys =
- zip_options xs ys handle ListPair.UnequalLengths =>
- err "more instantiations than variables in thm";
-
- val thm' =
- Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
- val thm'' =
- Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
- in thm'' end;
-
fun infer_instantiate' ctxt args th =
let
val vars = rev (Term.add_vars (Thm.full_prop_of th) []);
--- a/src/Pure/more_thm.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/Pure/more_thm.ML Mon Jul 27 17:44:55 2015 +0200
@@ -60,6 +60,7 @@
val elim_implies: thm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
+ val instantiate': ctyp option list -> cterm option list -> thm -> thm
val global_certify_inst: theory ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
@@ -354,6 +355,26 @@
end;
+(* instantiate by left-to-right occurrence of variables *)
+
+fun instantiate' cTs cts thm =
+ let
+ fun err msg =
+ raise TYPE ("instantiate': " ^ msg,
+ map_filter (Option.map Thm.typ_of) cTs,
+ map_filter (Option.map Thm.term_of) cts);
+
+ fun zip_vars xs ys =
+ zip_options xs ys handle ListPair.UnequalLengths =>
+ err "more instantiations than variables in thm";
+
+ val thm' =
+ Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
+ val thm'' =
+ Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
+ in thm'' end;
+
+
(* certify_instantiate *)
fun global_certify_inst thy (instT, inst) =
--- a/src/Tools/atomize_elim.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/Tools/atomize_elim.ML Mon Jul 27 17:44:55 2015 +0200
@@ -117,7 +117,7 @@
if is_Bound thesis then all_tac
else let
val cthesis = Thm.global_cterm_of thy thesis
- val rule = instantiate' [SOME (Thm.ctyp_of_cterm cthesis)] [NONE, SOME cthesis]
+ val rule = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cthesis)] [NONE, SOME cthesis]
@{thm meta_spec}
in
compose_tac ctxt (false, rule, 1) i