# HG changeset patch # User wenzelm # Date 1438011895 -7200 # Node ID 7664e0916eec4e8f8b462426287200196952eeba # Parent 57dd0b45fc2135f05dfef48974daa47e0d4fc6bf tuned signature; diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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 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 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Decision_Procs/commutative_ring_tac.ML --- 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) diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Decision_Procs/ferrante_rackoff.ML --- 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 = diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Decision_Procs/langford.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/HOLCF/Cfun.thy --- 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))); diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- 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) diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/HOLCF/Tools/cont_proc.ML --- 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 = diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/HOLCF/Tools/fixrec.ML --- 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} diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Import/import_rule.ML --- 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)))] diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Library/Code_Abstract_Nat.thy --- 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) diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Library/Countable.thy --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- 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)); diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Library/positivstellensatz.ML --- 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 \ bool"}) val x_v = (("x", 0), @{typ real}) diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Multivariate_Analysis/normarith.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Nominal/nominal_datatype.ML --- 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; diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Nominal/nominal_inductive.ML --- 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, diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Nominal/nominal_inductive2.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Nominal/nominal_permeq.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Probability/measurable.ML --- 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) diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/String.thy --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/BNF/bnf_def.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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); diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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])); diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/BNF/bnf_fp_util.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/BNF/bnf_gfp.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- 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, diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/BNF/bnf_lfp.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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; diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Function/function_context_tree.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Function/function_core.ML --- 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) diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Function/induction_schema.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Function/scnp_reconstruct.ML --- 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}])) diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Lifting/lifting_term.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Meson/meson.ML --- 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, diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Meson/meson_clausify.ML --- 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*) diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Metis/metis_tactic.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Old_Datatype/old_datatype.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Qelim/cooper.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Qelim/qelim.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Quotient/quotient_tacs.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Transfer/transfer.ML --- 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) diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Transfer/transfer_bnf.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/choice_specification.ML --- 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 = diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/cnf.ML --- 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 *) diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/code_evaluation.ML --- 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; diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/groebner.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/inductive_set.ML --- 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 = diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/int_arith.ML --- 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 = diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/numeral_simprocs.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/record.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/semiring_normalizer.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/Pure/axclass.ML --- 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 diff -r 57dd0b45fc21 -r 7664e0916eec src/Pure/drule.ML --- 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) []); diff -r 57dd0b45fc21 -r 7664e0916eec src/Pure/more_thm.ML --- 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) = diff -r 57dd0b45fc21 -r 7664e0916eec src/Tools/atomize_elim.ML --- 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