# HG changeset patch # User wenzelm # Date 1436101350 -7200 # Node ID 48dd1cefb4ae155252731eb8cd89fb926db50d2a # Parent f6e8293747fd0a8bc5146212990900c0a46107de simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored); diff -r f6e8293747fd -r 48dd1cefb4ae NEWS --- a/NEWS Fri Jul 03 16:19:45 2015 +0200 +++ b/NEWS Sun Jul 05 15:02:30 2015 +0200 @@ -234,6 +234,12 @@ command. Minor INCOMPATIBILITY, use 'function' instead. +** ML ** + +* Thm.instantiate (and derivatives) no longer require the LHS of the +instantiation to be certified: plain variables are given directly. + + New in Isabelle2015 (May 2015) ------------------------------ diff -r f6e8293747fd -r 48dd1cefb4ae src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Doc/Implementation/Logic.thy Sun Jul 05 15:02:30 2015 +0200 @@ -656,7 +656,8 @@ @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\ @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\ @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\ - @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\ + @{index_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list + -> thm -> thm"} \\ @{index_ML Thm.add_axiom: "Proof.context -> binding * term -> theory -> (string * thm) * theory"} \\ @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> diff -r f6e8293747fd -r 48dd1cefb4ae src/Doc/Implementation/Proof.thy --- a/src/Doc/Implementation/Proof.thy Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Doc/Implementation/Proof.thy Sun Jul 05 15:02:30 2015 +0200 @@ -108,7 +108,7 @@ @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\ @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ @{index_ML Variable.import: "bool -> thm list -> Proof.context -> - (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\ + ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context"} \\ @{index_ML Variable.focus: "term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context"} \\ \end{mldecls} diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Decision_Procs/approximation.ML --- a/src/HOL/Decision_Procs/approximation.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Decision_Procs/approximation.ML Sun Jul 05 15:02:30 2015 +0200 @@ -78,9 +78,9 @@ |> HOLogic.mk_list @{typ nat} |> Thm.cterm_of ctxt in - (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n), - (@{cpat "?prec::nat"}, p), - (@{cpat "?ss::nat list"}, s)]) + (rtac (Thm.instantiate ([], [((("n", 0), @{typ nat}), n), + ((("prec", 0), @{typ nat}), p), + ((("ss", 0), @{typ "nat list"}), s)]) @{thm "approx_form"}) i THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st end @@ -95,9 +95,9 @@ val s = vs |> map lookup_splitting |> hd |> Thm.cterm_of ctxt in - rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s), - (@{cpat "?t::nat"}, t), - (@{cpat "?prec::nat"}, p)]) + rtac (Thm.instantiate ([], [((("s", 0), @{typ nat}), s), + ((("t", 0), @{typ nat}), t), + ((("prec", 0), @{typ nat}), p)]) @{thm "approx_tse_form"}) i st end end diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Decision_Procs/ferrante_rackoff.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Jul 05 15:02:30 2015 +0200 @@ -58,6 +58,7 @@ funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) (funpow 4 Thm.dest_arg (Thm.cprop_of (hd minf))) |> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun) + |> apply2 (apply2 (dest_Var o Thm.term_of)) fun myfwd (th1, th2, th3, th4, th5) p1 p2 [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] = @@ -73,7 +74,7 @@ in (fw true th1 th_1 th_1', fw false th2 th_2 th_2', fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5') end - val U_v = (Thm.dest_arg o Thm.dest_arg o Thm.dest_arg1) (Thm.cprop_of qe) + val U_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 (Thm.cprop_of qe))))) fun main vs p = let val ((xn,ce),(x,fm)) = (case Thm.term_of p of diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Eisbach/eisbach_rule_insts.ML --- a/src/HOL/Eisbach/eisbach_rule_insts.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Jul 05 15:02:30 2015 +0200 @@ -57,7 +57,7 @@ fun add_inst (xi, t) (Ts, ts) = (case AList.lookup (op =) tyvars xi of - SOME S => ((certT (TVar (xi, S)), certT (Logic.dest_type t)) :: Ts, ts) + SOME S => (((xi, S), certT (Logic.dest_type t)) :: Ts, ts) | NONE => (case AList.lookup (op =) tvars xi of SOME T => (Ts, (cert (Var (xi, T)), cert t) :: ts) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Eisbach/match_method.ML Sun Jul 05 15:02:30 2015 +0200 @@ -440,10 +440,9 @@ val focus_schematics = #2 o Focus_Data.get; -fun add_focus_schematics cterms = +fun add_focus_schematics schematics = (Focus_Data.map o @{apply 3(2)}) - (fold (fn (Var (xi, T), t) => Vartab.update_new (xi, (T, t))) - (map (apply2 Thm.term_of) cterms)); + (fold (fn ((xi, T), ct) => Vartab.update_new (xi, (T, Thm.term_of ct))) schematics); (* focus params *) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Import/import_rule.ML Sun Jul 05 15:02:30 2015 +0200 @@ -161,11 +161,9 @@ let val tvars = Term.add_tvars (Thm.prop_of thm) [] val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars - val tvars = map TVar tvars val thy = Thm.theory_of_thm thm - fun inst ty = Thm.global_ctyp_of thy ty in - Thm.instantiate ((map inst tvars ~~ map inst tfrees), []) thm + Thm.instantiate ((tvars ~~ map (Thm.global_ctyp_of thy) tfrees), []) thm end fun def' constname rhs thy = @@ -264,11 +262,12 @@ val tys_before = Term.add_tfrees (Thm.prop_of th) [] val th1 = Thm.varifyT_global th val tys_after = Term.add_tvars (Thm.prop_of th1) [] - val tyinst = map2 (fn bef => fn iS => - (case try (assoc (TFree bef)) lambda of - SOME cty => (Thm.global_ctyp_of thy (TVar iS), cty) - | NONE => (Thm.global_ctyp_of thy (TVar iS), Thm.global_ctyp_of thy (TFree bef)) - )) tys_before tys_after + val tyinst = + map2 (fn bef => fn iS => + (case try (assoc (TFree bef)) lambda of + SOME cty => (iS, cty) + | NONE => (iS, Thm.global_ctyp_of thy (TFree bef)))) + tys_before tys_after in Thm.instantiate (tyinst,[]) th1 end @@ -334,9 +333,7 @@ val tns = map (fn (_, _) => "'") tvs val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt)) val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs)) - val cvs = map (Thm.ctyp_of ctxt) vs - val ctvs = map (Thm.ctyp_of ctxt) (map TVar tvs) - val thm' = Thm.instantiate ((ctvs ~~ cvs), []) thm + val thm' = Thm.instantiate ((tvs ~~ map (Thm.ctyp_of ctxt) vs), []) thm in snd (Global_Theory.add_thm ((binding, thm'), []) thy) end diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Library/Old_SMT/old_smt_normalize.ML --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Sun Jul 05 15:02:30 2015 +0200 @@ -34,7 +34,7 @@ fun inst f ct thm = let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) - in Thm.instantiate ([], [(cv, ct)]) thm end + in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end in fun instantiate_elim thm = @@ -215,7 +215,7 @@ fun insert_trigger_conv [] ct = Conv.all_conv ct | insert_trigger_conv ctss ct = let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct - in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end + in Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]) trigger_eq end fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct = let @@ -298,7 +298,8 @@ fun mk_weight_eq w = let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq) in - Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq + Thm.instantiate ([], [(dest_Var (Thm.term_of cv), Numeral.mk_cnumber @{ctyp int} w)]) + weight_eq end fun add_weight_conv NONE _ = Conv.all_conv diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Library/Old_SMT/old_smt_utils.ML --- a/src/HOL/Library/Old_SMT/old_smt_utils.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML Sun Jul 05 15:02:30 2015 +0200 @@ -152,7 +152,7 @@ val destT1 = hd o Thm.dest_ctyp val destT2 = hd o tl o Thm.dest_ctyp -fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct +fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct fun instT cU (cT, ct) = instTs [cU] ([cT], ct) fun instT' ct = instT (Thm.ctyp_of_cterm ct) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Library/Old_SMT/old_z3_proof_literals.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Sun Jul 05 15:02:30 2015 +0200 @@ -195,7 +195,9 @@ fun on_cprop f thm = f (Thm.cprop_of thm) fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm) fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 = - Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule + Thm.instantiate ([], + [(dest_Var (Thm.term_of cv1), on_cprop f thm1), + (dest_Var (Thm.term_of cv2), on_cprop g thm2)]) rule |> Old_Z3_Proof_Tools.discharge thm1 |> Old_Z3_Proof_Tools.discharge thm2 fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct) @@ -303,7 +305,7 @@ |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule))) end - val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE})) + val falseE_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE})))) fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE} in fun contradict conj ct = diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Library/Old_SMT/old_z3_proof_parser.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Sun Jul 05 15:02:30 2015 +0200 @@ -109,7 +109,7 @@ val max = fold (Integer.max o fst) vars 0 val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt) fun mk (i, v) = - (v, Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v))) + (dest_Var (Thm.term_of v), Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v))) in map mk vars end fun close ctxt (ct, vars) = @@ -161,7 +161,10 @@ if null vars then ([], vars) else fold part vars ([], []) - in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end + in + (Thm.instantiate_cterm ([], map (apfst (dest_Var o Thm.term_of)) inst) ct, + (maxidx', vars' @ all_vars)) + end in fun mk_fun f ts = let val (cts, (_, vars)) = fold_map prep ts (0, []) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Sun Jul 05 15:02:30 2015 +0200 @@ -625,7 +625,10 @@ val vs = frees_of ctxt (Thm.term_of ct) val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt val vars_of = get_vars Term.add_vars Var (K true) ctxt' - in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end + in + (Thm.instantiate ([], map (dest_Var o Thm.term_of) (vars_of (Thm.prop_of thm)) ~~ vs) thm, + ctxt') + end val sk_rules = @{lemma "c = (SOME x. P x) ==> (EX x. P x) = P c" diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Library/Old_SMT/old_z3_proof_tools.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Sun Jul 05 15:02:30 2015 +0200 @@ -27,7 +27,7 @@ (Proof.context -> cterm -> thm) -> cterm -> thm (*a faster COMP*) - type compose_data + type compose_data = cterm list * (cterm -> cterm list) * thm val precompose: (cterm -> cterm list) -> thm -> compose_data val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data val compose: compose_data -> thm -> thm @@ -257,11 +257,11 @@ fun list2 (x, y) = [x, y] -fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule) -fun precompose2 f rule = precompose (list2 o f) rule +fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule) +fun precompose2 f rule : compose_data = precompose (list2 o f) rule fun compose (cvs, f, rule) thm = - discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule) + discharge thm (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Library/cconv.ML --- a/src/HOL/Library/cconv.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Library/cconv.ML Sun Jul 05 15:02:30 2015 +0200 @@ -182,7 +182,7 @@ ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct | _ => cv ct) -fun inst_imp_cong ct = Thm.instantiate ([], [(@{cpat "?A :: prop"}, ct)]) Drule.imp_cong +fun inst_imp_cong ct = Thm.instantiate ([], [((("A", 0), propT), ct)]) Drule.imp_cong (*rewrite B in A1 \ ... \ An \ B*) fun concl_cconv 0 cv ct = cv ct @@ -202,10 +202,10 @@ NONE => (As, B) | SOME (A,B) => strip_prems (i - 1) (A::As) B val (prem, (prems, concl)) = ct |> Thm.dest_implies ||> strip_prems n [] - val rewr_imp_concl = Thm.instantiate ([], [(@{cpat "?C :: prop"}, concl)]) @{thm rewr_imp} + val rewr_imp_concl = Thm.instantiate ([], [((("C", 0), propT), concl)]) @{thm rewr_imp} val th1 = cv prem RS rewr_imp_concl val nprems = Thm.nprems_of th1 - fun inst_cut_rl ct = Thm.instantiate ([], [(@{cpat "?psi :: prop"}, ct)]) cut_rl + fun inst_cut_rl ct = Thm.instantiate ([], [((("psi", 0), propT), ct)]) cut_rl fun f p th = (th RS inst_cut_rl p) |> Conv.fconv_rule (Conv.concl_conv nprems (Conv.rewr_conv @{thm imp_cong_eq})) in fold f prems th1 end diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Library/old_recdef.ML Sun Jul 05 15:02:30 2015 +0200 @@ -304,15 +304,15 @@ (Pv, Dv, Sign.typ_match thy (Dty, ty) Vartab.empty) | _ => error "not a valid case thm"; - val type_cinsts = map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T)) + val type_cinsts = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest type_insts); - val cPv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Pv); - val cDv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Dv); + val Pv = dest_Var (Envir.subst_term_types type_insts Pv); + val Dv = dest_Var (Envir.subst_term_types type_insts Dv); in Conv.fconv_rule Drule.beta_eta_conversion (case_thm |> Thm.instantiate (type_cinsts, []) - |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])) + |> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)])) end; @@ -1124,11 +1124,11 @@ local (* this is fragile *) val prop = Thm.prop_of spec val x = hd (tl (Misc_Legacy.term_vars prop)) - val cTV = Thm.ctyp_of @{context} (type_of x) + val TV = dest_TVar (type_of x) val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec in fun SPEC tm thm = - let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_cterm tm)], []) gspec + let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec in thm RS (Thm.forall_elim tm gspec') end end; @@ -1141,11 +1141,11 @@ local val prop = Thm.prop_of allI val [P] = Misc_Legacy.add_term_vars (prop, []) - fun cty_theta ctxt = map (fn (i, (S, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (i, S), ty)) + fun cty_theta ctxt = map (fn (i, (S, ty)) => ((i, S), Thm.ctyp_of ctxt ty)) fun ctm_theta ctxt = map (fn (i, (_, tm2)) => let val ctm2 = Thm.cterm_of ctxt tm2 - in (Thm.cterm_of ctxt (Var (i, Thm.typ_of_cterm ctm2)), ctm2) end) + in ((i, Thm.typ_of_cterm ctm2), ctm2) end) fun certify ctxt (ty_theta,tm_theta) = (cty_theta ctxt (Vartab.dest ty_theta), ctm_theta ctxt (Vartab.dest tm_theta)) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Sun Jul 05 15:02:30 2015 +0200 @@ -483,7 +483,7 @@ fun real_not_eq_conv ct = let val (l,r) = dest_eq (Thm.dest_arg ct) - val th = Thm.instantiate ([],[(@{cpat "?x::real"},l),(@{cpat "?y::real"},r)]) neq_th + val th = Thm.instantiate ([],[((("x", 0), @{typ real}),l),((("y", 0), @{typ real}),r)]) neq_th val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th))) val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p val th_n = fconv_rule (arg_conv poly_neg_conv) th_x @@ -729,9 +729,9 @@ val pth_max = instantiate' [SOME @{ctyp real}] [] max_split val pth_min = instantiate' [SOME @{ctyp real}] [] min_split val abs_tm = @{cterm "abs :: real => _"} - val p_tm = @{cpat "?P :: real => bool"} - val x_tm = @{cpat "?x :: real"} - val y_tm = @{cpat "?y::real"} + val p_v = (("P", 0), @{typ "real \ bool"}) + val x_v = (("x", 0), @{typ real}) + val y_v = (("y", 0), @{typ real}) val is_max = is_binop @{cterm "max :: real => _"} val is_min = is_binop @{cterm "min :: real => _"} fun is_abs t = is_comb t andalso Thm.dest_fun t aconvc abs_tm @@ -746,16 +746,16 @@ val elim_abs = eliminate_construct is_abs (fn p => fn ax => - Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax)]) pth_abs) + Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax)]) pth_abs) val elim_max = eliminate_construct is_max (fn p => fn ax => let val (ax,y) = Thm.dest_comb ax - in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)]) + in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)]) pth_max end) val elim_min = eliminate_construct is_min (fn p => fn ax => let val (ax,y) = Thm.dest_comb ax - in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)]) + in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)]) pth_min end) in first_conv [elim_abs, elim_max, elim_min, all_conv] end; diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Library/rewrite.ML --- a/src/HOL/Library/rewrite.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Library/rewrite.ML Sun Jul 05 15:02:30 2015 +0200 @@ -265,15 +265,13 @@ let fun instantiate_normalize_env ctxt env thm = let - fun certs f = map (apply2 (f ctxt)) val prop = Thm.prop_of thm val norm_type = Envir.norm_type o Envir.type_env val insts = Term.add_vars prop [] - |> map (fn x as (s,T) => (Var (s, norm_type env T), Envir.norm_term env (Var x))) - |> certs Thm.cterm_of + |> map (fn x as (s, T) => + ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x)))) val tyinsts = Term.add_tvars prop [] - |> map (fn x => (TVar x, norm_type env (TVar x))) - |> certs Thm.ctyp_of + |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x)))) in Drule.instantiate_normalize (tyinsts, insts) thm end fun unify_with_rhs context to env thm = diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Matrix_LP/Compute_Oracle/linker.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Sun Jul 05 15:02:30 2015 +0200 @@ -315,8 +315,8 @@ end fun conv_subst thy (subst : Type.tyenv) = - map (fn (iname, (sort, ty)) => (Thm.global_ctyp_of thy (TVar (iname, sort)), Thm.global_ctyp_of thy ty)) - (Vartab.dest subst) + map (fn (iname, (sort, ty)) => ((iname, sort), Thm.global_ctyp_of thy ty)) + (Vartab.dest subst) fun add_monos thy monocs pats ths = let diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Sun Jul 05 15:02:30 2015 +0200 @@ -258,8 +258,9 @@ local val pth_zero = @{thm norm_zero} - val tv_n = (Thm.ctyp_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of) - pth_zero + val tv_n = + (dest_TVar o Thm.typ_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of) + pth_zero val concl = Thm.dest_arg o Thm.cprop_of fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = let @@ -356,7 +357,7 @@ val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (#hyps (Thm.crep_thm th1)) val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1]) val cps = map (swap o Thm.dest_equals) (cprems_of th11) - val th12 = Drule.instantiate_normalize ([], cps) th11 + val th12 = Drule.instantiate_normalize ([], map (apfst (dest_Var o Thm.term_of)) cps) th11 val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12; in hd (Variable.export ctxt' ctxt [th13]) end diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Sun Jul 05 15:02:30 2015 +0200 @@ -1390,13 +1390,13 @@ end); val induct_aux' = Thm.instantiate ([], - map (fn (s, v as Var (_, T)) => - (Thm.global_cterm_of thy9 v, Thm.global_cterm_of thy9 (Free (s, T)))) + map (fn (s, Var (v as (_, T))) => + (v, Thm.global_cterm_of thy9 (Free (s, T)))) (pnames ~~ map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct_aux)))) @ map (fn (_, f) => let val f' = Logic.varify_global f - in (Thm.global_cterm_of thy9 f', + in (dest_Var f', Thm.global_cterm_of thy9 (Const (@{const_name Nominal.supp}, fastype_of f'))) end) fresh_fs) induct_aux; @@ -1562,7 +1562,7 @@ (augment_sort thy1 pt_cp_sort (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P))) (fn {context = ctxt, ...} => dtac (Thm.instantiate ([], - [(Thm.global_cterm_of thy11 (Var (("pi", 0), permT)), + [((("pi", 0), permT), Thm.global_cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths) in (ths, ths') end) dt_atomTs); @@ -1653,7 +1653,7 @@ SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY [cut_facts_tac [rec_prem] 1, rtac (Thm.instantiate ([], - [(Thm.global_cterm_of thy11 (Var (("pi", 0), mk_permT aT)), + [((("pi", 0), mk_permT aT), Thm.global_cterm_of thy11 (perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th) 1, asm_simp_tac (put_simpset HOL_ss context addsimps @@ -1872,8 +1872,7 @@ val l = find_index (equal T) dt_atomTs; val th = nth (nth rec_equiv_thms' l) k; val th' = Thm.instantiate ([], - [(Thm.global_cterm_of thy11 (Var (("pi", 0), U)), - Thm.global_cterm_of thy11 p)]) th; + [((("pi", 0), U), Thm.global_cterm_of thy11 p)]) th; in rtac th' 1 end; val th' = Goal.prove context'' [] [] (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y)) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sun Jul 05 15:02:30 2015 +0200 @@ -31,7 +31,10 @@ (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) fun res_inst_tac_term ctxt = - gen_res_inst_tac_term ctxt (curry Thm.instantiate); + gen_res_inst_tac_term ctxt (fn instT => fn inst => + Thm.instantiate + (map (apfst (dest_TVar o Thm.typ_of)) instT, + map (apfst (dest_Var o Thm.term_of)) inst)); fun res_inst_tac_term' ctxt = gen_res_inst_tac_term ctxt (K Drule.cterm_instantiate) []; @@ -146,10 +149,10 @@ fun inst_fresh vars params i st = let val vars' = Misc_Legacy.term_vars (Thm.prop_of st); in case subtract (op =) vars vars' of - [x] => + [Var v] => Seq.single (Thm.instantiate ([], - [apply2 (Thm.cterm_of ctxt) (x, fold_rev Term.abs params (Bound 0))]) st) + [(v, Thm.cterm_of ctxt (fold_rev Term.abs params (Bound 0)))]) st) | _ => error "fresh_fun_simp: Too many variables, please report." end in diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Sun Jul 05 15:02:30 2015 +0200 @@ -338,7 +338,8 @@ val pis'' = fold (concat_perm #> map) pis' pis; val env = Pattern.first_order_match thy (ihypt, Thm.prop_of ihyp) (Vartab.empty, Vartab.empty); - val ihyp' = Thm.instantiate ([], map (apply2 (Thm.global_cterm_of thy)) + val ihyp' = Thm.instantiate ([], + map (fn (v, t) => (dest_Var v, Thm.global_cterm_of thy t)) (map (Envir.subst_term env) vs ~~ map (fold_rev (NominalDatatype.mk_perm []) (rev pis' @ pis)) params' @ [z])) ihyp; diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Jul 05 15:02:30 2015 +0200 @@ -146,9 +146,7 @@ fun inst_params thy (vs, p) th cts = let val env = Pattern.first_order_match thy (p, Thm.prop_of th) (Vartab.empty, Vartab.empty) - in Thm.instantiate ([], - map (Envir.subst_term env #> Thm.global_cterm_of thy) vs ~~ cts) th - end; + in Thm.instantiate ([], map (dest_Var o Envir.subst_term env) vs ~~ cts) th end; fun prove_strong_ind s alt_name avoids ctxt = let diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Sun Jul 05 15:02:30 2015 +0200 @@ -95,7 +95,11 @@ fun mapT_and_recertify ct = (Thm.cterm_of ctxt (Term.map_types (Term.map_type_tvar substT) (Thm.term_of ct))); val insts' = map (apfst mapT_and_recertify) insts; - in Thm.instantiate (instTs, insts') end; + in + Thm.instantiate + (map (apfst (dest_TVar o Thm.typ_of)) instTs, + map (apfst (dest_Var o Thm.term_of)) insts') + end; fun tvar_clash ixn S S' = raise TYPE ("Type variable has two distinct sorts", [TVar (ixn, S), TVar (ixn, S')], []); @@ -145,9 +149,9 @@ val (tyinsts,insts) = fold naive_cterm_first_order_match (Thm.prems_of rule ~~ map Thm.cprop_of prems) ([], []); val tyinsts' = - map (fn (v, (S, U)) => apply2 (Thm.ctyp_of ctxt) (TVar (v, S), U)) tyinsts; + map (fn (v, (S, U)) => ((v, S), Thm.ctyp_of ctxt U)) tyinsts; val insts' = - map (fn (idxn, ct) => (Thm.cterm_of ctxt (Var (idxn, Thm.typ_of_cterm ct)), ct)) insts; + map (fn (idxn, ct) => ((idxn, Thm.typ_of_cterm ct), ct)) insts; val rule' = Thm.instantiate (tyinsts', insts') rule; in fold Thm.elim_implies prems rule' end; @@ -286,7 +290,7 @@ @{thm subtract_Tip} |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; val [alpha] = ct |> Thm.ctyp_of_cterm |> Thm.dest_ctyp; - in (alpha, #1 (dest_Var (Thm.term_of ct))) end; + in (dest_TVar (Thm.typ_of alpha), #1 (dest_Var (Thm.term_of ct))) end; in fun subtractProver ctxt (Const (@{const_name Tip}, T)) ct dist_thm = @@ -296,7 +300,7 @@ in Thm.instantiate ([(alpha, Thm.ctyp_of ctxt alphaI)], - [(Thm.cterm_of ctxt (Var (v, treeT alphaI)), ct')]) @{thm subtract_Tip} + [((v, treeT alphaI), ct')]) @{thm subtract_Tip} end | subtractProver ctxt (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm = let diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Sun Jul 05 15:02:30 2015 +0200 @@ -570,14 +570,14 @@ diff (Proof_Context.theory_of ctxt) (scheme_t, instance_t) (*valuation of type variables*) - val typeval = map (apply2 (Thm.ctyp_of ctxt)) type_pairing + val typeval = map (fn (v, T) => (dest_TVar v, Thm.ctyp_of ctxt T)) type_pairing val typeval_env = map (apfst dest_TVar) type_pairing (*valuation of term variables*) val termval = - map (apfst (type_devar typeval_env)) term_pairing - |> map (apply2 (Thm.cterm_of ctxt)) + map (apfst (dest_Var o type_devar typeval_env)) term_pairing + |> map (apsnd (Thm.cterm_of ctxt)) in Thm.instantiate (typeval, termval) scheme_thm end diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Jul 05 15:02:30 2015 +0200 @@ -950,8 +950,8 @@ val tactic = if is_none var_opt then no_tac else - fold (curry (op APPEND)) (map (instantiate_tac (the var_opt)) skolem_cts) no_tac - + fold (curry (op APPEND)) + (map (instantiate_tac (dest_Var (Thm.term_of (the var_opt)))) skolem_cts) no_tac in tactic st end diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Jul 05 15:02:30 2015 +0200 @@ -607,9 +607,9 @@ let val n = Thm.nprems_of coind; val m = Thm.nprems_of (hd rel_monos) - n; - fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi))))) - |> apply2 (Thm.cterm_of ctxt); - val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var); + fun mk_inst phi = + (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi)))))) + val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst; fun mk_unfold rel_eq rel_mono = let val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl]; diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun Jul 05 15:02:30 2015 +0200 @@ -685,7 +685,9 @@ let val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat; - val rho_As = map (apply2 (Thm.ctyp_of lthy)) (map Logic.varifyT_global As ~~ As); + val rho_As = + map (fn (T, U) => (dest_TVar T, Thm.ctyp_of lthy U)) + (map Logic.varifyT_global As ~~ As); fun inst_thm t thm = Drule.instantiate' [] [SOME (Thm.cterm_of lthy t)] diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Sun Jul 05 15:02:30 2015 +0200 @@ -200,7 +200,8 @@ val (P_var, x_var) = Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> strip_comb |> apsnd hd - val P_rangeT = range_type (snd (Term.dest_Var P_var)) + |> apply2 dest_Var + val P_rangeT = range_type (snd P_var) val PT = map (snd o dest_Free) args ---> P_rangeT val x_inst = cert (foldl1 HOLogic.mk_prod args) val P_inst = cert (uncurry_n (length args) (Free (P, PT))) @@ -211,7 +212,7 @@ THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 THEN CONVERSION (split_params_conv ctxt then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3) - |> Thm.instantiate ([], [(cert P_var, P_inst), (cert x_var, x_inst)]) + |> Thm.instantiate ([], [(P_var, P_inst), (x_var, x_inst)]) |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt) |> singleton (Variable.export ctxt' ctxt) in diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Function/relation.ML --- a/src/HOL/Tools/Function/relation.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Function/relation.ML Sun Jul 05 15:02:30 2015 +0200 @@ -18,8 +18,7 @@ fun inst_state_tac ctxt inst = SUBGOAL (fn (goal, _) => (case Term.add_vars goal [] of - [v as (_, T)] => - PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))])) + [v as (_, T)] => PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (inst T))])) | _ => no_tac)); fun relation_tac ctxt rel i = @@ -39,9 +38,7 @@ |> map_types Type_Infer.paramify_vars |> Type.constraint T |> Syntax.check_term ctxt; - in - PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt rel')])) - end + in PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt rel')])) end | _ => no_tac)); fun relation_infer_tac ctxt rel i = diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Lifting/lifting_bnf.ML --- a/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Sun Jul 05 15:02:30 2015 +0200 @@ -23,7 +23,7 @@ fun get_lhs thm = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd)) val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars - val inst = map2 (curry (apply2 (Thm.cterm_of ctxt))) vars UNIVs + val inst = map dest_Var vars ~~ map (Thm.cterm_of ctxt) UNIVs val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst) |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)} |> (fn thm => thm RS sym) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Sun Jul 05 15:02:30 2015 +0200 @@ -310,7 +310,7 @@ val thy = Proof_Context.theory_of ctxt val (_, qty_schematic) = quot_thm_rty_qty quot_thm val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty - fun prep_ty (x, (S, ty)) = apply2 (Thm.ctyp_of ctxt) (TVar (x, S), ty) + fun prep_ty (x, (S, ty)) = ((x, S), Thm.ctyp_of ctxt ty) val ty_inst = Vartab.fold (cons o prep_ty) match_env [] in Thm.instantiate (ty_inst, []) quot_thm diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Lifting/lifting_util.ML --- a/src/HOL/Tools/Lifting/lifting_util.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Sun Jul 05 15:02:30 2015 +0200 @@ -145,7 +145,7 @@ fun instT_thm ctxt env = let val cinst = env |> Vartab.dest - |> map (fn (x, (S, T)) => (Thm.ctyp_of ctxt (TVar (x, S)), Thm.ctyp_of ctxt T)); + |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T)); in Thm.instantiate (cinst, []) end; diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Sun Jul 05 15:02:30 2015 +0200 @@ -346,16 +346,17 @@ (*Replaces universally quantified variables by FREE variables -- because assumptions may not contain scheme variables. Later, generalize using Variable.export. *) local - val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec)))); - val spec_varT = Thm.typ_of_cterm spec_var; - fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu; + val spec_var = + Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec)))) + |> Thm.term_of |> dest_Var; + fun name_of (Const (@{const_name All}, _) $ Abs(x, _, _)) = x | name_of _ = Name.uu; in fun freeze_spec th ctxt = let val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt; val spec' = spec - |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, spec_varT)))]); + |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]); in (th RS spec', ctxt') end end; diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Sun Jul 05 15:02:30 2015 +0200 @@ -44,10 +44,10 @@ "Sledgehammer_Util".) *) fun transform_elim_theorem th = (case Thm.concl_of th of (*conclusion variable*) - @{const Trueprop} $ (v as Var (_, @{typ bool})) => - Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, cfalse)]) th - | v as Var(_, @{typ prop}) => - Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, ctp_false)]) th + @{const Trueprop} $ (Var (v as (_, @{typ bool}))) => + Thm.instantiate ([], [(v, cfalse)]) th + | Var (v as (_, @{typ prop})) => + Thm.instantiate ([], [(v, ctp_false)]) th | _ => th) @@ -375,9 +375,7 @@ th ctxt val (cnf_ths, ctxt) = clausify nnf_th fun intr_imp ct th = - Thm.instantiate ([], map (apply2 (Thm.cterm_of ctxt)) - [(Var (("i", 0), @{typ nat}), - HOLogic.mk_nat ax_no)]) + Thm.instantiate ([], [((("i", 0), @{typ nat}), Thm.cterm_of ctxt (HOLogic.mk_nat ax_no))]) (zero_var_indexes @{thm skolem_COMBK_D}) RS Thm.implies_intr ct th in diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Jul 05 15:02:30 2015 +0200 @@ -174,7 +174,7 @@ fun incr_type_indexes ctxt inc th = let val tvs = Term.add_tvars (Thm.full_prop_of th) [] - fun inc_tvar ((a, i), s) = apply2 (Thm.ctyp_of ctxt) (TVar ((a, i), s), TVar ((a, i + inc), s)) + fun inc_tvar ((a, i), s) = (((a, i), s), Thm.ctyp_of ctxt (TVar ((a, i + inc), s))) in Thm.instantiate (map inc_tvar tvs, []) th end @@ -211,7 +211,7 @@ |> rpair (Envir.empty ~1) |-> fold (Pattern.unify (Context.Proof ctxt)) |> Envir.type_env |> Vartab.dest - |> map (fn (x, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T)) + |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T)) in (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as @@ -400,8 +400,8 @@ val thy = Proof_Context.theory_of ctxt val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) - fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (v, S), T) - fun mk (v, (T, t)) = apply2 (Thm.cterm_of ctxt) (Var (v, Envir.subst_type tyenv T), t) + fun mkT (v, (S, T)) = ((v, S), Thm.ctyp_of ctxt T) + fun mk (v, (T, t)) = ((v, Envir.subst_type tyenv T), Thm.cterm_of ctxt t) val instsT = Vartab.fold (cons o mkT) tyenv [] val insts = Vartab.fold (cons o mk) tenv [] @@ -570,11 +570,11 @@ Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0, tenv = Vartab.empty, tyenv = tyenv} val ty_inst = - Vartab.fold (fn (x, (S, T)) => cons (apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T))) + Vartab.fold (fn (x, (S, T)) => cons (((x, S), Thm.ctyp_of ctxt T))) tyenv [] val t_inst = [apply2 (Thm.cterm_of ctxt o Envir.norm_term env) (Var var, t')] in - Drule.instantiate_normalize (ty_inst, t_inst) th + Drule.instantiate_normalize (ty_inst, map (apfst (dest_Var o Thm.term_of)) t_inst) th end | _ => raise Fail "expected a single non-zapped, non-Metis Var") in diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Sun Jul 05 15:02:30 2015 +0200 @@ -232,10 +232,10 @@ fun instantiate i n ({context = ctxt2, prems, ...}: Subgoal.focus) = let - fun term_pair_of (ix, (ty, t)) = (Var (ix, ty), t) + fun inst_pair_of (ix, (ty, t)) = ((ix, ty), t) fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty) - |> snd |> Vartab.dest |> map (apply2 (Thm.cterm_of ctxt2) o term_pair_of) + |> snd |> Vartab.dest |> map (apsnd (Thm.cterm_of ctxt2) o inst_pair_of) val (cases, (eqs, prems1)) = apsnd (chop (nargs - nparams)) (chop n prems) val case_th = rewrite_rule ctxt2 (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1)) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Sun Jul 05 15:02:30 2015 +0200 @@ -150,10 +150,10 @@ val get_pmi = get_pmi_term o Thm.cprop_of; -val p_v' = @{cpat "?P' :: int => bool"}; -val q_v' = @{cpat "?Q' :: int => bool"}; -val p_v = @{cpat "?P:: int => bool"}; -val q_v = @{cpat "?Q:: int => bool"}; +val p_v' = (("P'", 0), @{typ "int \ bool"}); +val q_v' = (("Q'", 0), @{typ "int \ bool"}); +val p_v = (("P", 0), @{typ "int \ bool"}); +val q_v = (("Q", 0), @{typ "int \ bool"}); fun myfwd (th1, th2, th3) p q [(th_1,th_2,th_3), (th_1',th_2',th_3')] = @@ -430,11 +430,13 @@ val insert_tm = @{cterm "insert :: int => _"}; fun mkISet cts = fold_rev (Thm.apply insert_tm #> Thm.apply) cts emptyIS; val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1; -val [A_tm,B_tm] = map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg - |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg) - [asetP,bsetP]; +val [A_v,B_v] = + map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg + |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg + |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg + |> Thm.term_of |> dest_Var) [asetP, bsetP]; -val D_tm = @{cpat "?D::int"}; +val D_v = (("D", 0), @{typ int}); fun cooperex_conv ctxt vs q = let @@ -501,16 +503,16 @@ if length (distinct (op aconv) bl) <= length (distinct (op aconv) al) then (bl,b0,decomp_minf, - fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp) + fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_v,B), (D_v,cd)]) th) dp) [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@ - (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)])) + (map (Thm.instantiate ([],[(B_v,B), (D_v,cd)])) [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj, bsetdisj,infDconj, infDdisj]), cpmi) else (al,a0,decomp_pinf,fn A => - (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp) + (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_v,A), (D_v,cd)]) th) dp) [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@ - (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)])) + (map (Thm.instantiate ([],[(A_v,A), (D_v,cd)])) [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj, asetdisj,infDconj, infDdisj]),cppi) val cpth = diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sun Jul 05 15:02:30 2015 +0200 @@ -73,7 +73,9 @@ val lhs = eq |> Thm.dest_arg1; val pt_random_aux = lhs |> Thm.dest_fun; val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun; -val aT = pt_random_aux |> Thm.ctyp_of_cterm |> dest_ctyp_nth 1; +val a_v = + pt_random_aux |> Thm.ctyp_of_cterm |> dest_ctyp_nth 1 + |> Thm.typ_of |> dest_TVar; val rew_thms = map mk_meta_eq [@{thm natural_zero_minus_one}, @{thm Suc_natural_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}]; @@ -89,7 +91,7 @@ (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; val Type (_, [_, iT]) = T; val icT = Thm.ctyp_of lthy iT; - val inst = Thm.instantiate_cterm ([(aT, icT)], []); + val inst = Thm.instantiate_cterm ([(a_v, icT)], []); fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t); val t_rhs = lambda t_k proto_t_rhs; val eqs0 = [subst_v @{term "0::natural"} eq, @@ -98,11 +100,11 @@ val ((_, (_, eqs2)), lthy') = lthy |> BNF_LFP_Compat.primrec_simple [((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1; - val cT_random_aux = inst pt_random_aux; - val cT_rhs = inst pt_rhs; + val cT_random_aux = inst pt_random_aux |> Thm.term_of |> dest_Var; + val cT_rhs = inst pt_rhs |> Thm.term_of |> dest_Var; val rule = @{thm random_aux_rec} |> Drule.instantiate_normalize - ([(aT, icT)], + ([(a_v, icT)], [(cT_random_aux, Thm.cterm_of lthy' t_random_aux), (cT_rhs, Thm.cterm_of lthy' t_rhs)]); fun tac ctxt = diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Jul 05 15:02:30 2015 +0200 @@ -72,20 +72,16 @@ | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing." -fun prep_trm thy (x, (T, t)) = - (Thm.global_cterm_of thy (Var (x, T)), Thm.global_cterm_of thy t) - -fun prep_ty thy (x, (S, ty)) = - (Thm.global_ctyp_of thy (TVar (x, S)), Thm.global_ctyp_of thy ty) - fun get_match_inst thy pat trm = let val univ = Unify.matchers (Context.Theory thy) [(pat, trm)] val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *) val tenv = Vartab.dest (Envir.term_env env) val tyenv = Vartab.dest (Envir.type_env env) + fun prep_ty (x, (S, ty)) = ((x, S), Thm.global_ctyp_of thy ty) + fun prep_trm (x, (T, t)) = ((x, T), Thm.global_cterm_of thy t) in - (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) + (map prep_ty tyenv, map prep_trm tenv) end (* Calculates the instantiations for the lemmas: @@ -480,7 +476,7 @@ then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm) else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm) val thm4 = - Drule.instantiate_normalize ([], [(Thm.cterm_of ctxt insp, Thm.cterm_of ctxt inst)]) thm3 + Drule.instantiate_normalize ([], [(dest_Var insp, Thm.cterm_of ctxt inst)]) thm3 in Conv.rewr_conv thm4 ctrm end diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Sun Jul 05 15:02:30 2015 +0200 @@ -35,7 +35,7 @@ fun inst f ct thm = let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) - in Thm.instantiate ([], [(cv, ct)]) thm end + in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end in fun instantiate_elim thm = @@ -199,8 +199,10 @@ fun insert_trigger_conv [] ct = Conv.all_conv ct | insert_trigger_conv ctss ct = - let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct - in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end + let + val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct + val inst = map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)] + in Thm.instantiate ([], inst) trigger_eq end fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct = let diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/SMT/smt_util.ML --- a/src/HOL/Tools/SMT/smt_util.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/SMT/smt_util.ML Sun Jul 05 15:02:30 2015 +0200 @@ -171,7 +171,7 @@ val destT1 = hd o Thm.dest_ctyp val destT2 = hd o tl o Thm.dest_ctyp -fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct +fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct fun instT cU (cT, ct) = instTs [cU] ([cT], ct) fun instT' ct = instT (Thm.ctyp_of_cterm ct) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/SMT/z3_replay_methods.ML --- a/src/HOL/Tools/SMT/z3_replay_methods.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Sun Jul 05 15:02:30 2015 +0200 @@ -100,20 +100,20 @@ (Vartab.empty, Vartab.empty) |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t) -fun gen_certify_inst sel mk cert ctxt thm t = +fun gen_certify_inst sel cert ctxt thm t = let val inst = match ctxt (dest_thm thm) (dest_prop t) - fun cert_inst (ix, (a, b)) = (cert (mk (ix, a)), cert b) + fun cert_inst (ix, (a, b)) = ((ix, a), cert b) in Vartab.fold (cons o cert_inst) (sel inst) [] end fun match_instantiateT ctxt t thm = if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then - Thm.instantiate (gen_certify_inst fst TVar (Thm.ctyp_of ctxt) ctxt thm t, []) thm + Thm.instantiate (gen_certify_inst fst (Thm.ctyp_of ctxt) ctxt thm t, []) thm else thm fun match_instantiate ctxt t thm = let val thm' = match_instantiateT ctxt t thm in - Thm.instantiate ([], gen_certify_inst snd Var (Thm.cterm_of ctxt) ctxt thm' t) thm' + Thm.instantiate ([], gen_certify_inst snd (Thm.cterm_of ctxt) ctxt thm' t) thm' end fun apply_rule ctxt t = diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/SMT/z3_replay_util.ML --- a/src/HOL/Tools/SMT/z3_replay_util.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/SMT/z3_replay_util.ML Sun Jul 05 15:02:30 2015 +0200 @@ -15,7 +15,7 @@ val discharge: thm -> thm -> thm (*a faster COMP*) - type compose_data + type compose_data = cterm list * (cterm -> cterm list) * thm val precompose: (cterm -> cterm list) -> thm -> compose_data val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data val compose: compose_data -> thm -> thm @@ -71,11 +71,12 @@ fun list2 (x, y) = [x, y] -fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule) -fun precompose2 f rule = precompose (list2 o f) rule +fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule) +fun precompose2 f rule : compose_data = precompose (list2 o f) rule fun compose (cvs, f, rule) thm = - discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule) + discharge thm + (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule) (* simpset *) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Sun Jul 05 15:02:30 2015 +0200 @@ -592,11 +592,10 @@ fun prep a = the (AList.lookup (op =) tab a) val thm = transfer_rule_of_terms fst ctxt' tab s t val binsts = bool_insts (if equiv then 0 else 1) (s, t) - val cbool = @{ctyp bool} - val relT = @{typ "bool => bool => bool"} val idx = Thm.maxidx_of thm + 1 - fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool) - fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t) + fun tinst (a, _) = (((a, idx), @{sort type}), @{ctyp bool}) + fun inst (a, t) = + ((Name.clean_index (prep a, idx), @{typ "bool \ bool \ bool"}), Thm.cterm_of ctxt' t) in thm |> Thm.generalize (tfrees, rnames @ frees) idx @@ -616,11 +615,10 @@ fun prep a = the (AList.lookup (op =) tab a) val thm = transfer_rule_of_terms snd ctxt' tab t s val binsts = bool_insts 1 (s, t) - val cbool = @{ctyp bool} - val relT = @{typ "bool => bool => bool"} val idx = Thm.maxidx_of thm + 1 - fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool) - fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t) + fun tinst (a, _) = (((a, idx), @{sort type}), @{ctyp bool}) + fun inst (a, t) = + ((Name.clean_index (prep a, idx), @{typ "bool \ bool \ bool"}), Thm.cterm_of ctxt' t) in thm |> Thm.generalize (tfrees, rnames @ frees) idx diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/coinduction.ML --- a/src/HOL/Tools/coinduction.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/coinduction.ML Sun Jul 05 15:02:30 2015 +0200 @@ -61,9 +61,9 @@ |> fold Variable.declare_names vars |> fold Variable.declare_thm (raw_thm :: prems); val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl; - val (rhoTs, rhots) = Thm.match (thm_concl, concl) - |>> map (apply2 Thm.typ_of) - ||> map (apply2 Thm.term_of); + val (instT, inst) = Thm.match (thm_concl, concl); + val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT; + val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst; val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd |> map (subst_atomic_types rhoTs); val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs; @@ -160,4 +160,3 @@ end; end; - diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/hologic.ML Sun Jul 05 15:02:30 2015 +0200 @@ -207,14 +207,14 @@ let val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ) handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]); - val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]); + val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]); in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end; fun conj_elim ctxt thPQ = let val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ)) handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]); - val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]); + val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]); val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ; val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ; in (thP, thQ) end; diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/inductive_set.ML Sun Jul 05 15:02:30 2015 +0200 @@ -205,7 +205,7 @@ val x' = map_type (K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x; in - (Thm.cterm_of ctxt x, + (dest_Var x, Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts (HOLogic.Collect_const U $ HOLogic.mk_psplits ps U HOLogic.boolT @@ -367,7 +367,7 @@ val T = HOLogic.mk_ptupleT ps Us; val x' = map_type (K (Rs ---> HOLogic.mk_setT T)) x in - (Thm.cterm_of ctxt x, + (dest_Var x, Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (k downto 0)), list_comb (x', map Bound (l - 1 downto k + 1)))))) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/lin_arith.ML Sun Jul 05 15:02:30 2015 +0200 @@ -60,10 +60,8 @@ fun is_nat t = (fastype_of1 t = HOLogic.natT); fun mk_nat_thm thy t = - let - val cn = Thm.global_cterm_of thy (Var (("n", 0), HOLogic.natT)) - and ct = Thm.global_cterm_of thy t - in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end; + let val ct = Thm.global_cterm_of thy t + in Drule.instantiate_normalize ([], [((("n", 0), HOLogic.natT), ct)]) @{thm le0} end; end; diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/monomorph.ML --- a/src/HOL/Tools/monomorph.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/monomorph.ML Sun Jul 05 15:02:30 2015 +0200 @@ -159,7 +159,7 @@ fun instantiate ctxt subst = let - fun cert (ix, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (ix, S), T) + fun cert (ix, (S, T)) = ((ix, S), Thm.ctyp_of ctxt T) fun cert' subst = Vartab.fold (cons o cert) subst [] in Thm.instantiate (cert' subst, []) end diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/numeral.ML Sun Jul 05 15:02:30 2015 +0200 @@ -49,7 +49,7 @@ val uminus = @{cpat "uminus"}; val uminusT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm uminus)); -fun instT T V = Thm.instantiate_cterm ([(V, T)], []); +fun instT T V = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of V), T)], []); in diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Sun Jul 05 15:02:30 2015 +0200 @@ -595,8 +595,8 @@ fun prove_nz ctxt T t = let - val z = Thm.instantiate_cterm ([(zT,T)],[]) zr - val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq + val z = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of zT), T)],[]) zr + val eq = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of eqT), T)],[]) geq val th = Simplifier.rewrite (ctxt addsimps @{thms simp_thms}) (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply eq t) z))) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/record.ML Sun Jul 05 15:02:30 2015 +0200 @@ -1755,7 +1755,7 @@ fun mk_eq_refl thy = @{thm equal_refl} |> Thm.instantiate - ([apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], []) + ([((("'a", 0), @{sort equal}), Thm.global_ctyp_of thy (Logic.varifyT_global extT))], []) |> Axclass.unoverload thy; val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq); val ensure_exhaustive_record = diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/reification.ML --- a/src/HOL/Tools/reification.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/reification.ML Sun Jul 05 15:02:30 2015 +0200 @@ -169,9 +169,9 @@ val (fnvs, invs) = List.partition (fn ((vn, _),_) => member (op =) vns vn) (Vartab.dest tmenv); val (fts, its) = (map (snd o snd) fnvs, - map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of ctxt) (Var ((vn, vi), tT), t)) invs); + map (fn ((vn, vi), (tT, t)) => (((vn, vi), tT), Thm.cterm_of ctxt t)) invs); val ctyenv = - map (fn ((vn, vi), (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar ((vn, vi), s), ty)) + map (fn ((vn, vi), (s, ty)) => (((vn, vi), s), Thm.ctyp_of ctxt ty)) (Vartab.dest tyenv); in ((map (Thm.cterm_of ctxt) fts ~~ replicate (length fts) ctxt, @@ -203,7 +203,7 @@ val sbst = Envir.subst_term (tyenv, tmenv); val sbsT = Envir.subst_type tyenv; val subst_ty = - map (fn (n, (s, t)) => apply2 (Thm.ctyp_of ctxt'') (TVar (n, s), t)) (Vartab.dest tyenv) + map (fn (n, (s, t)) => ((n, s), Thm.ctyp_of ctxt'' t)) (Vartab.dest tyenv) val tml = Vartab.dest tmenv; val (subst_ns, bds) = fold_map (fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds => @@ -230,7 +230,9 @@ let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, [])); in map (apply2 ih) (subst_ns @ subst_vs @ cts) end; - val th = (Drule.instantiate_normalize (subst_ty, substt) eq) RS sym; + val th = + (Drule.instantiate_normalize (subst_ty, map (apfst (dest_Var o Thm.term_of)) substt) eq) + RS sym; in (hd (Variable.export ctxt'' ctxt [th]), bds) end) handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds); @@ -266,10 +268,7 @@ let val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |> strip_comb; - val subst = - map_filter - (fn (v as Var (_, T)) => SOME (Thm.cterm_of ctxt' v, subst T) - | _ => NONE) vs; + val subst = map_filter (fn Var v => SOME (v, subst (#2 v)) | _ => NONE) vs; in Thm.instantiate ([], subst) eq end; val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs; val bds = AList.make (K ([], [])) tys; @@ -285,9 +284,10 @@ | is_list_var _ = false; val vars = th |> Thm.prop_of |> Logic.dest_equals |> snd |> strip_comb |> snd |> filter is_list_var; - val vs = map (fn v as Var (_, T) => + val vs = map (fn Var (v as (_, T)) => (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars; - val th' = Drule.instantiate_normalize ([], map (apply2 (Thm.cterm_of ctxt)) vs) th; + val th' = + Drule.instantiate_normalize ([], map (apsnd (Thm.cterm_of ctxt)) vs) th; val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th')); in Thm.transitive th'' th' end; diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/sat.ML Sun Jul 05 15:02:30 2015 +0200 @@ -73,8 +73,6 @@ val resolution_thm = @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)} -val cP = Thm.cterm_of @{context} (Var (("P", 0), HOLogic.boolT)); - (* ------------------------------------------------------------------------- *) (* lit_ord: an order on integers that considers their absolute values only, *) (* thereby treating integers that represent the same atom (positively *) @@ -173,7 +171,7 @@ val cLit = snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *) in - Thm.instantiate ([], [(cP, cLit)]) resolution_thm + Thm.instantiate ([], [((("P", 0), HOLogic.boolT), cLit)]) resolution_thm end val _ = diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/semiring_normalizer.ML Sun Jul 05 15:02:30 2015 +0200 @@ -238,7 +238,7 @@ if is_binop ct ct' then Thm.dest_binop ct' else raise CTERM ("dest_binop: bad binop", [ct, ct']) -fun inst_thm inst = Thm.instantiate ([], inst); +fun inst_thm inst = Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) inst); val dest_number = Thm.term_of #> HOLogic.dest_number #> snd; val is_number = can dest_number; @@ -300,7 +300,7 @@ val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat) val neg_tm = Thm.dest_fun neg_pat val dest_sub = dest_binop sub_tm - in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub, neg_mul |> concl |> Thm.dest_arg, + in (neg_mul, sub_add, sub_tm, neg_tm, dest_sub, neg_mul |> concl |> Thm.dest_arg, sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg) end | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), true_tm, true_tm)); @@ -760,7 +760,7 @@ fun polynomial_neg_conv ctxt tm = let val (l,r) = Thm.dest_comb tm in if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else - let val th1 = inst_thm [(cx',r)] neg_mul + let val th1 = inst_thm [(cx', r)] neg_mul val th2 = Thm.transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1)) in Thm.transitive th2 (polynomial_monomial_mul_conv ctxt (concl th2)) end @@ -770,7 +770,7 @@ (* Subtraction. *) fun polynomial_sub_conv ctxt tm = let val (l,r) = dest_sub tm - val th1 = inst_thm [(cx',l),(cy',r)] sub_add + val th1 = inst_thm [(cx', l), (cy', r)] sub_add val (tm1,tm2) = Thm.dest_comb(concl th1) val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv ctxt tm2) in Thm.transitive th1 (Thm.transitive th2 (polynomial_add_conv ctxt (concl th2))) diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/split_rule.ML Sun Jul 05 15:02:30 2015 +0200 @@ -42,7 +42,7 @@ fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl = let val T' = HOLogic.flatten_tupleT T1 ---> T2; val newt = ap_split T1 T2 (Var (v, T')); - in Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (t, newt)]) rl end + in Thm.instantiate ([], [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end | split_rule_var' _ _ rl = rl; @@ -65,15 +65,15 @@ val ys = Name.variant_list xs (replicate (length Ts) a); in (xs @ ys, - apply2 (Thm.cterm_of ctxt) - (v, HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T - (map (Var o apfst (rpair 0)) (ys ~~ Ts))) :: insts) + (dest_Var v, + Thm.cterm_of ctxt (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T + (map (Var o apfst (rpair 0)) (ys ~~ Ts)))) :: insts) end | mk_tuple _ x = x; val newt = ap_split' Us U (Var (v, T')); val (vs', insts) = fold mk_tuple ts (vs, []); in - (Drule.instantiate_normalize ([], [apply2 (Thm.cterm_of ctxt) (t, newt)] @ insts) rl, vs') + (Drule.instantiate_normalize ([], ((v, T), Thm.cterm_of ctxt newt) :: insts) rl, vs') end | complete_split_rule_var _ _ x = x; diff -r f6e8293747fd -r 48dd1cefb4ae src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Sun Jul 05 15:02:30 2015 +0200 @@ -424,7 +424,7 @@ val T = Thm.typ_of_cterm cv in mth - |> Thm.instantiate ([], [(cv, number_of T n)]) + |> Thm.instantiate ([], [(dest_Var (Thm.term_of cv), number_of T n)]) |> rewrite_concl |> discharge_prem handle CTERM _ => mult_by_add n thm diff -r f6e8293747fd -r 48dd1cefb4ae src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Provers/hypsubst.ML Sun Jul 05 15:02:30 2015 +0200 @@ -186,10 +186,10 @@ val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U)); in compose_tac ctxt (true, Drule.instantiate_normalize (instT, - map (apply2 (Thm.cterm_of ctxt)) - [(Var (ixn, Ts ---> U --> body_type T), u), - (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t), - (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl', + map (apsnd (Thm.cterm_of ctxt)) + [((ixn, Ts ---> U --> body_type T), u), + ((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t), + ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl', Thm.nprems_of rl) i end | NONE => no_tac); diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/Isar/element.ML Sun Jul 05 15:02:30 2015 +0200 @@ -201,7 +201,7 @@ SOME C => let val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C); - val th' = Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (C, thesis)]) th; + val th' = Thm.instantiate ([], [(Term.dest_Var C, Thm.cterm_of ctxt thesis)]) th; in (th', true) end | NONE => (th, false)); @@ -340,7 +340,7 @@ fun instantiate_tfrees thy subst th = let val idx = Thm.maxidx_of th + 1; - fun cert_inst (a, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar ((a, idx), S), T); + fun cert_inst (a, (S, T)) = (((a, idx), S), Thm.global_ctyp_of thy T); fun add_inst (a, S) insts = if AList.defined (op =) insts a then insts diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/Isar/generic_target.ML Sun Jul 05 15:02:30 2015 +0200 @@ -271,12 +271,13 @@ |>> map Logic.dest_type; val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees); - val inst = filter (is_Var o fst) (vars ~~ frees); - val cinstT = instT - |> map (apply2 (Thm.ctyp_of ctxt) o apfst TVar); - val cinst = inst - |> map (apply2 (Thm.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT))); - val result' = Thm.instantiate (cinstT, cinst) result; + val inst = + map_filter + (fn (Var (xi, T), t) => + SOME ((xi, Term_Subst.instantiateT instT T), + Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t)) + | _ => NONE) (vars ~~ frees); + val result' = Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt)) instT, inst) result; (*import assumes/defines*) val result'' = diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/Isar/obtain.ML Sun Jul 05 15:02:30 2015 +0200 @@ -334,7 +334,7 @@ val instT = fold (Term.add_tvarsT o #2) params [] - |> map (TVar #> (fn T => apply2 (Thm.ctyp_of ctxt) (T, norm_type T))); + |> map (fn v => (v, Thm.ctyp_of ctxt (norm_type (TVar v)))); val closed_rule = rule |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) |> Thm.instantiate (instT, []); diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/Isar/subgoal.ML --- a/src/Pure/Isar/subgoal.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/Isar/subgoal.ML Sun Jul 05 15:02:30 2015 +0200 @@ -12,8 +12,9 @@ signature SUBGOAL = sig - type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, - asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list} + type focus = + {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list, + concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list} val focus_params: Proof.context -> int -> thm -> focus * thm val focus_params_fixed: Proof.context -> int -> thm -> focus * thm val focus_prems: Proof.context -> int -> thm -> focus * thm @@ -36,8 +37,9 @@ (* focus *) -type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, - asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}; +type focus = + {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list, + concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}; fun gen_focus (do_prems, do_concl) ctxt i raw_st = let @@ -100,7 +102,7 @@ val (inst1, inst2) = split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys)); - val th'' = Thm.instantiate ([], inst1) th'; + val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th'; in ((inst2, th''), ctxt'') end; (* diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/Proof/proof_checker.ML Sun Jul 05 15:02:30 2015 +0200 @@ -78,8 +78,8 @@ let val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev; val (fmap, thm') = Thm.varifyT_global' [] thm; - val ctye = map (apply2 (Thm.global_ctyp_of thy)) - (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) + val ctye = + (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts); in Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm')) end; @@ -118,7 +118,7 @@ handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t end - | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) = + | thm_of (vs, names) Hs (AbsP (_, SOME t, prf)) = let val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t)); val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf; diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/Tools/rule_insts.ML Sun Jul 05 15:02:30 2015 +0200 @@ -149,8 +149,8 @@ in thm |> Drule.instantiate_normalize - (map (apply2 (Thm.ctyp_of ctxt') o apfst TVar) inst_tvars, - map (apply2 (Thm.cterm_of ctxt') o apfst Var) inst_vars) + (map (apsnd (Thm.ctyp_of ctxt')) inst_tvars, + map (apsnd (Thm.cterm_of ctxt')) inst_vars) |> singleton (Variable.export ctxt' ctxt) |> Rule_Cases.save thm end; @@ -240,13 +240,13 @@ val inc = Thm.maxidx_of st + 1; val lift_type = Logic.incr_tvar inc; - fun lift_var ((a, j), T) = Var ((a, j + inc), paramTs ---> lift_type T); + fun lift_var ((a, j), T) = ((a, j + inc), paramTs ---> lift_type T); fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t); val inst_tvars' = inst_tvars - |> map (apply2 (Thm.ctyp_of inst_ctxt o lift_type) o apfst TVar); + |> map (fn (((a, i), S), T) => (((a, i + inc), S), Thm.ctyp_of inst_ctxt (lift_type T))); val inst_vars' = inst_vars - |> map (fn (v, t) => apply2 (Thm.cterm_of inst_ctxt) (lift_var v, lift_term t)); + |> map (fn (v, t) => (lift_var v, Thm.cterm_of inst_ctxt (lift_term t))); val thm' = Thm.lift_rule cgoal thm |> Drule.instantiate_normalize (inst_tvars', inst_vars') @@ -262,10 +262,11 @@ fun make_elim_preserve ctxt rl = let val maxidx = Thm.maxidx_of rl; + fun var x = ((x, 0), propT); fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT)); val revcut_rl' = - Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)), - (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl; + Drule.instantiate_normalize ([], [(var "V", cvar ("V", maxidx + 1)), + (var "W", cvar ("W", maxidx + 1))]) Drule.revcut_rl; in (case Seq.list_of (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/conjunction.ML --- a/src/Pure/conjunction.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/conjunction.ML Sun Jul 05 15:02:30 2015 +0200 @@ -69,8 +69,8 @@ local -val A = read_prop "A" and vA = read_prop "?A"; -val B = read_prop "B" and vB = read_prop "?B"; +val A = read_prop "A" and vA = (("A", 0), propT); +val B = read_prop "B" and vB = (("B", 0), propT); val C = read_prop "C"; val ABC = read_prop "A ==> B ==> C"; val A_B = read_prop "A &&& B"; diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/drule.ML Sun Jul 05 15:02:30 2015 +0200 @@ -20,7 +20,8 @@ val lift_all: Proof.context -> cterm -> thm -> thm val implies_elim_list: thm -> thm list -> thm val implies_intr_list: cterm list -> thm -> thm - val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm + val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> + thm -> thm val zero_var_indexes_list: thm list -> thm list val zero_var_indexes: thm -> thm val implies_intr_hyps: thm -> thm @@ -613,11 +614,9 @@ fun mk_term ct = let - val thy = Thm.theory_of_cterm ct; - val T = Thm.typ_of_cterm ct; - val instT = apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), []), T); - val x = Thm.global_cterm_of thy (Var (("x", 0), T)); - in Thm.instantiate ([instT], [(x, ct)]) termI end; + val cT = Thm.ctyp_of_cterm ct; + val T = Thm.typ_of cT; + in Thm.instantiate ([((("'a", 0), []), cT)], [((("x", 0), T), ct)]) termI end; fun dest_term th = let val cprop = strip_imp_concl (Thm.cprop_of th) in @@ -767,9 +766,9 @@ val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0); val instT = Vartab.fold (fn (xi, (S, T)) => - cons (apply2 (Thm.global_ctyp_of thy) (TVar (xi, S), Envir.norm_type tye T))) tye []; + cons ((xi, S), Thm.global_ctyp_of thy (Envir.norm_type tye T))) tye []; val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs; - in instantiate_normalize (instT, inst) th end + in instantiate_normalize (instT, map (apfst (Thm.term_of #> dest_Var)) inst) th end handle TERM (msg, _) => raise THM (msg, 0, [th]) | TYPE (msg, _, _) => raise THM (msg, 0, [th]); end; @@ -784,27 +783,18 @@ map_filter (Option.map Thm.typ_of) cTs, map_filter (Option.map Thm.term_of) cts); - fun inst_of (v, ct) = - (Thm.global_cterm_of (Thm.theory_of_cterm ct) (Var v), ct) - handle TYPE (msg, _, _) => err msg; - - fun tyinst_of (v, cT) = - (Thm.global_ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT) - handle TYPE (msg, _, _) => err msg; - fun zip_vars xs ys = zip_options xs ys handle ListPair.UnequalLengths => err "more instantiations than variables in thm"; - (*instantiate types first!*) val thm' = if forall is_none cTs then thm - else Thm.instantiate - (map tyinst_of (zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm; + else + Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm; val thm'' = if forall is_none cts then thm' - else Thm.instantiate - ([], map inst_of (zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts)) thm'; + else + Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm'; in thm'' end; diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/goal.ML Sun Jul 05 15:02:30 2015 +0200 @@ -60,9 +60,7 @@ -------- (init) C ==> #C *) -val init = - let val A = #1 (Thm.dest_implies (Thm.cprop_of Drule.protectI)) - in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end; +fun init C = Thm.instantiate ([], [((("A", 0), propT), C)]) Drule.protectI; (* A1 ==> ... ==> An ==> C @@ -134,8 +132,7 @@ val fixes = map (Thm.cterm_of ctxt) xs; val tfrees = fold Term.add_tfrees (prop :: As) []; - val instT = - map (fn (a, S) => apply2 (Thm.ctyp_of ctxt) (TVar ((a, 0), S), TFree (a, S))) tfrees; + val instT = map (fn (a, S) => (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))) tfrees; val global_prop = Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))) diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/more_thm.ML Sun Jul 05 15:02:30 2015 +0200 @@ -62,12 +62,12 @@ val forall_elim_vars: int -> thm -> thm val global_certify_inst: theory -> ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> - (ctyp * ctyp) list * (cterm * cterm) list + ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list val global_certify_instantiate: theory -> ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm val certify_inst: Proof.context -> ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> - (ctyp * ctyp) list * (cterm * cterm) list + ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list val certify_instantiate: Proof.context -> ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm val forall_intr_frees: thm -> thm @@ -357,15 +357,15 @@ (* certify_instantiate *) fun global_certify_inst thy (instT, inst) = - (map (fn (v, T) => apply2 (Thm.global_ctyp_of thy) (TVar v, T)) instT, - map (fn (v, t) => apply2 (Thm.global_cterm_of thy) (Var v, t)) inst); + (map (apsnd (Thm.global_ctyp_of thy)) instT, + map (apsnd (Thm.global_cterm_of thy)) inst); fun global_certify_instantiate thy insts th = Thm.instantiate (global_certify_inst thy insts) th; fun certify_inst ctxt (instT, inst) = - (map (fn (v, T) => apply2 (Thm.ctyp_of ctxt) (TVar v, T)) instT, - map (fn (v, t) => apply2 (Thm.cterm_of ctxt) (Var v, t)) inst); + (map (apsnd (Thm.ctyp_of ctxt)) instT, + map (apsnd (Thm.cterm_of ctxt)) inst); fun certify_instantiate ctxt insts th = Thm.instantiate (certify_inst ctxt insts) th; @@ -446,10 +446,12 @@ fun stripped_sorts thy t = let - val tfrees = rev (map TFree (Term.add_tfrees t [])); - val tfrees' = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT (length tfrees)); - val strip = tfrees ~~ tfrees'; - val recover = map (apply2 (Thm.global_ctyp_of thy o Logic.varifyT_global) o swap) strip; + val tfrees = rev (Term.add_tfrees t []); + val tfrees' = map (fn a => (a, [])) (Name.invent Name.context Name.aT (length tfrees)); + val recover = + map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) + tfrees' tfrees; + val strip = map (apply2 TFree) (tfrees ~~ tfrees'); val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; in (strip, recover, t') end; diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/raw_simplifier.ML Sun Jul 05 15:02:30 2015 +0200 @@ -1044,8 +1044,9 @@ then NONE else SOME thm2')) end; -val (cA, (cB, cC)) = - apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong))); +val vA = (("A", 0), propT); +val vB = (("B", 0), propT); +val vC = (("C", 0), propT); fun transitive1 NONE NONE = NONE | transitive1 (SOME thm1) NONE = SOME thm1 @@ -1177,7 +1178,7 @@ val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq); val eq' = Thm.implies_elim - (Thm.instantiate ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong) + (Thm.instantiate ([], [(vA, prem), (vB, lhs), (vC, rhs)]) Drule.imp_cong) (Thm.implies_intr prem eq); in if not r then eq' @@ -1188,9 +1189,9 @@ in Thm.transitive (Thm.transitive - (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) Drule.swap_prems_eq) + (Thm.instantiate ([], [(vA, prem'), (vB, prem), (vC, concl)]) Drule.swap_prems_eq) eq') - (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) Drule.swap_prems_eq) + (Thm.instantiate ([], [(vA, prem), (vB, prem''), (vC, concl)]) Drule.swap_prems_eq) end end diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/thm.ML Sun Jul 05 15:02:30 2015 +0200 @@ -47,8 +47,10 @@ val lambda: cterm -> cterm -> cterm val adjust_maxidx_cterm: int -> cterm -> cterm val incr_indexes_cterm: int -> cterm -> cterm - val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list - val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list + val match: cterm * cterm -> + ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list + val first_order_match: cterm * cterm -> + ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list (*theorems*) val rep_thm: thm -> {thy: theory, @@ -120,8 +122,10 @@ val equal_elim: thm -> thm -> thm val flexflex_rule: Proof.context option -> thm -> thm Seq.seq val generalize: string list * string list -> int -> thm -> thm - val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm - val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm + val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> + thm -> thm + val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> + cterm -> cterm val trivial: cterm -> thm val of_class: ctyp * class -> thm val strip_shyps: thm -> thm @@ -312,12 +316,10 @@ val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); val sorts = Sorts.union sorts1 sorts2; fun mk_cTinst ((a, i), (S, T)) = - (Ctyp {T = TVar ((a, i), S), thy = thy, maxidx = i, sorts = sorts}, - Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts}); - fun mk_ctinst ((x, i), (T, t)) = - let val T = Envir.subst_type Tinsts T in - (Cterm {t = Var ((x, i), T), T = T, thy = thy, maxidx = i, sorts = sorts}, - Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts}) + (((a, i), S), Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts}); + fun mk_ctinst ((x, i), (U, t)) = + let val T = Envir.subst_type Tinsts U in + (((x, i), T), Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts}) end; in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; @@ -1091,37 +1093,28 @@ fun pretty_typing thy t T = Pretty.block [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T]; -fun add_inst (ct, cu) (thy, sorts) = +fun add_inst (v as (_, T), cu) (thy, sorts) = let - val Cterm {t = t, T = T, ...} = ct; - val Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; - val thy' = Theory.merge (thy, merge_thys0 ct cu); + val Cterm {t = u, T = U, thy = thy2, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; + val thy' = Theory.merge (thy, thy2); val sorts' = Sorts.union sorts_u sorts; in - (case t of Var v => - if T = U then ((v, (u, maxidx_u)), (thy', sorts')) - else raise TYPE (Pretty.string_of (Pretty.block + if T = U then ((v, (u, maxidx_u)), (thy', sorts')) + else + raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", - Pretty.fbrk, pretty_typing thy' t T, - Pretty.fbrk, pretty_typing thy' u U]), [T, U], [t, u]) - | _ => raise TYPE (Pretty.string_of (Pretty.block - [Pretty.str "instantiate: not a variable", - Pretty.fbrk, Syntax.pretty_term_global thy' t]), [], [t])) + Pretty.fbrk, pretty_typing thy' (Var v) T, + Pretty.fbrk, pretty_typing thy' u U]), [T, U], [Var v, u]) end; -fun add_instT (cT, cU) (thy, sorts) = +fun add_instT (v as (_, S), cU) (thy, sorts) = let - val Ctyp {T, thy = thy1, ...} = cT - and Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; - val thy' = Theory.merge (thy, Theory.merge (thy1, thy2)); + val Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; + val thy' = Theory.merge (thy, thy2); val sorts' = Sorts.union sorts_U sorts; in - (case T of TVar (v as (_, S)) => - if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts')) - else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], []) - | _ => raise TYPE (Pretty.string_of (Pretty.block - [Pretty.str "instantiate: not a type variable", - Pretty.fbrk, Syntax.pretty_typ_global thy' T]), [T], [])) + if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts')) + else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], []) end; in diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/variable.ML --- a/src/Pure/variable.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Pure/variable.ML Sun Jul 05 15:02:30 2015 +0200 @@ -71,10 +71,11 @@ (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context val importT_terms: term list -> Proof.context -> term list * Proof.context val import_terms: bool -> term list -> Proof.context -> term list * Proof.context - val importT: thm list -> Proof.context -> ((ctyp * ctyp) list * thm list) * Proof.context + val importT: thm list -> Proof.context -> + (((indexname * sort) * ctyp) list * thm list) * Proof.context val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context val import: bool -> thm list -> Proof.context -> - (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context + ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list val focus_params: term -> Proof.context -> (string list * (string * typ) list) * Proof.context diff -r f6e8293747fd -r 48dd1cefb4ae src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Tools/IsaPlanner/rw_inst.ML Sun Jul 05 15:02:30 2015 +0200 @@ -174,7 +174,7 @@ val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); (* certified instantiations for types *) - val ctyp_insts = map (fn (ix, (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (ix, s), ty)) typinsts; + val ctyp_insts = map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts; (* type instantiated versions *) val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; @@ -198,7 +198,7 @@ (* create certms of instantiations *) val cinsts_tyinst = - map (fn (ix, (ty, t)) => apply2 (Thm.cterm_of ctxt) (Var (ix, ty), t)) insts_tyinst_inst; + map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst; (* The instantiated rule *) val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst); @@ -217,7 +217,7 @@ val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst); val (cprems, abstract_rule_inst) = rule_inst - |> Thm.instantiate ([], cterm_renamings) + |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings) |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst; val specific_tgt_rule = Conv.fconv_rule Drule.beta_eta_conversion @@ -227,7 +227,7 @@ val tgt_th_inst = tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst) - |> Thm.instantiate ([], cterm_renamings); + |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings); val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; in diff -r f6e8293747fd -r 48dd1cefb4ae src/Tools/coherent.ML --- a/src/Tools/coherent.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Tools/coherent.ML Sun Jul 05 15:02:30 2015 +0200 @@ -179,10 +179,10 @@ val th' = Drule.implies_elim_list (Thm.instantiate - (map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T)) (Vartab.dest tye), + (map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye), map (fn (ixn, (T, t)) => - apply2 (Thm.cterm_of ctxt) (Var (ixn, Envir.subst_type tye T), t)) (Vartab.dest env) @ - map (fn (ixnT, t) => apply2 (Thm.cterm_of ctxt) (Var ixnT, t)) insts) th) + ((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @ + map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts) th) (map (nth asms) is); val (_, cases) = dest_elim (Thm.prop_of th'); in diff -r f6e8293747fd -r 48dd1cefb4ae src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Tools/induct.ML Sun Jul 05 15:02:30 2015 +0200 @@ -573,8 +573,8 @@ val pairs = Vartab.dest (Envir.term_env env); val types = Vartab.dest (Envir.type_env env); val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs; - val xs = map2 (curry (Thm.cterm_of ctxt o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts); - in (map (fn (xi, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (xi, S), T)) types, xs ~~ ts) end; + val xs = map #1 pairs ~~ map Thm.typ_of_cterm ts; + in (map (fn (ai, (S, T)) => ((ai, S), Thm.ctyp_of ctxt T)) types, xs ~~ ts) end; in diff -r f6e8293747fd -r 48dd1cefb4ae src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Tools/misc_legacy.ML Sun Jul 05 15:02:30 2015 +0200 @@ -173,9 +173,9 @@ then ((v, T), true, free_of "METAHYP2_" (v, T)) else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T)) (*Instantiate subgoal vars by Free applied to params*) - fun mk_ctpair (v, in_concl, u) = - if in_concl then apply2 (Thm.cterm_of ctxt) (Var v, u) - else apply2 (Thm.cterm_of ctxt) (Var v, list_comb (u, fparams)) + fun mk_inst (v, in_concl, u) = + if in_concl then (v, Thm.cterm_of ctxt u) + else (v, Thm.cterm_of ctxt (list_comb (u, fparams))) (*Restore Vars with higher type and index*) fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) = if in_concl then apply2 (Thm.cterm_of ctxt) (u, Var ((a, i), T)) @@ -191,7 +191,7 @@ fold Term.add_vars (Logic.strip_imp_prems prop) [] and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [] val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars - val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st + val st' = Thm.instantiate ([], map mk_inst subgoal_insts) st val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st') val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs) in (*restore the unknowns to the hypotheses*) @@ -269,7 +269,7 @@ fun thaw i th' = (*i is non-negative increment for Var indexes*) th' |> forall_intr_list (map #2 insts) |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts) - in (Thm.instantiate ([],insts) fth, thaw) end + in (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw) end end; (*Basic version of the function above. No option to rename Vars apart in thaw. @@ -291,7 +291,7 @@ fun thaw th' = th' |> forall_intr_list (map #2 insts) |> forall_elim_list (map #1 insts) - in (Thm.instantiate ([],insts) fth, thaw) end + in (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw) end end; end; diff -r f6e8293747fd -r 48dd1cefb4ae src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/Tools/nbe.ML Sun Jul 05 15:02:30 2015 +0200 @@ -101,11 +101,10 @@ val vs_tab = map mk_entry (Term.add_tfrees (Thm.term_of ct) []); fun instantiate thm = let - val cert_tvars = map (Thm.ctyp_of ctxt o TVar) (Term.add_tvars - ((fst o Logic.dest_equals o Logic.strip_imp_concl o Thm.prop_of) thm) []); - val instantiation = - map2 (fn cert_tvar => fn (_, (_, (cT, _))) => (cert_tvar, cT)) cert_tvars vs_tab; - in Thm.instantiate (instantiation, []) thm end; + val tvars = + Term.add_tvars (#1 (Logic.dest_equals (Logic.strip_imp_concl (Thm.prop_of thm)))) []; + val instT = map2 (fn v => fn (_, (_, (cT, _))) => (v, cT)) tvars vs_tab; + in Thm.instantiate (instT, []) thm end; fun of_class (TFree (v, _), class) = the (AList.lookup (op =) ((snd o snd o the o AList.lookup (op =) vs_tab) v) class) | of_class (T, _) = error ("Bad type " ^ Syntax.string_of_typ ctxt T); diff -r f6e8293747fd -r 48dd1cefb4ae src/ZF/Tools/cartprod.ML --- a/src/ZF/Tools/cartprod.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/ZF/Tools/cartprod.ML Sun Jul 05 15:02:30 2015 +0200 @@ -109,7 +109,7 @@ in remove_split ctxt (Drule.instantiate_normalize ([], - [apply2 (Thm.cterm_of ctxt) (Var(v, Ind_Syntax.iT-->T2), newt)]) rl) + [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl) end | split_rule_var _ (t,T,rl) = rl; diff -r f6e8293747fd -r 48dd1cefb4ae src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/ZF/Tools/inductive_package.ML Sun Jul 05 15:02:30 2015 +0200 @@ -495,7 +495,7 @@ The name "x.1" comes from the "RS spec" !*) val inst = case elem_frees of [_] => I - | _ => Drule.instantiate_normalize ([], [(Thm.global_cterm_of thy (Var(("x",1), Ind_Syntax.iT)), + | _ => Drule.instantiate_normalize ([], [(((("x",1), Ind_Syntax.iT)), Thm.global_cterm_of thy elem_tuple)]); (*strip quantifier and the implication*)