# HG changeset patch # User wenzelm # Date 1433246143 -7200 # Node ID 5568b16aa477e42c5e5ab42d69b596c2de052d9c # Parent befdc10ebb4299d388dfae0f79a86f4a36338025 clarified context; diff -r befdc10ebb42 -r 5568b16aa477 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 02 11:03:02 2015 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 02 13:55:43 2015 +0200 @@ -171,11 +171,10 @@ (* INFERENCE RULE: RESOLVE *) (*Increment the indexes of only the type variables*) -fun incr_type_indexes inc th = +fun incr_type_indexes ctxt inc th = let val tvs = Term.add_tvars (Thm.full_prop_of th) [] - val thy = Thm.theory_of_thm th - fun inc_tvar ((a, i), s) = apply2 (Thm.global_ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s)) + fun inc_tvar ((a, i), s) = apply2 (Thm.ctyp_of ctxt) (TVar ((a, i), s), TVar ((a, i + inc), s)) in Thm.instantiate (map inc_tvar tvs, []) th end @@ -185,7 +184,7 @@ Instantiations of those Vars could then fail. *) fun resolve_inc_tyvars ctxt tha i thb = let - val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha + val tha = incr_type_indexes ctxt (1 + Thm.maxidx_of thb) tha fun res (tha, thb) = (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true} (false, tha, Thm.nprems_of tha) i thb @@ -393,16 +392,16 @@ | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r) -fun flexflex_first_order th = +fun flexflex_first_order ctxt th = (case Thm.tpairs_of th of [] => th | pairs => let - val thy = Thm.theory_of_thm th + 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.global_ctyp_of thy) (TVar (v, S), T) - fun mk (v, (T, t)) = apply2 (Thm.global_cterm_of thy) (Var (v, Envir.subst_type tyenv T), t) + 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) val instsT = Vartab.fold (cons o mkT) tyenv [] val insts = Vartab.fold (cons o mk) tenv [] @@ -462,7 +461,7 @@ val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf) - |> flexflex_first_order + |> flexflex_first_order ctxt |> resynchronize ctxt fol_th val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) val _ = trace_msg ctxt (fn () => "=============================================") diff -r befdc10ebb42 -r 5568b16aa477 src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Tue Jun 02 11:03:02 2015 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Tue Jun 02 13:55:43 2015 +0200 @@ -32,28 +32,28 @@ (* for use when there are no prems to the subgoal *) (* does a case split on the given variable *) -fun mk_casesplit_goal_thm sgn (vstr,ty) gt = +fun mk_casesplit_goal_thm ctxt (vstr,ty) gt = let - val x = Free(vstr,ty) + val thy = Proof_Context.theory_of ctxt; + + val x = Free(vstr,ty); val abst = Abs(vstr, ty, Term.abstract_over (x, gt)); - val ctermify = Thm.global_cterm_of sgn; - val ctypify = Thm.global_ctyp_of sgn; - val case_thm = case_thm_of_ty sgn ty; + val case_thm = case_thm_of_ty thy ty; - val abs_ct = ctermify abst; - val free_ct = ctermify x; + val abs_ct = Thm.cterm_of ctxt abst; + val free_ct = Thm.cterm_of ctxt x; val (Pv, Dv, type_insts) = case (Thm.concl_of case_thm) of - (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => + (_ $ (Pv $ (Dv as Var(D, Dty)))) => (Pv, Dv, - Sign.typ_match sgn (Dty, ty) Vartab.empty) + Sign.typ_match thy (Dty, ty) Vartab.empty) | _ => error "not a valid case thm"; - val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T)) + val type_cinsts = map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T)) (Vartab.dest type_insts); - val cPv = ctermify (Envir.subst_term_types type_insts Pv); - val cDv = ctermify (Envir.subst_term_types type_insts Dv); + 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); in Conv.fconv_rule Drule.beta_eta_conversion (case_thm @@ -117,7 +117,6 @@ fun splitto ctxt splitths genth = let val _ = not (null splitths) orelse error "splitto: no given splitths"; - val thy = Thm.theory_of_thm genth; (* check if we are a member of splitths - FIXME: quicker and more flexible with discrim net. *) @@ -134,7 +133,7 @@ | SOME v => let val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th))); - val split_thm = mk_casesplit_goal_thm thy v gt; + val split_thm = mk_casesplit_goal_thm ctxt v gt; val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm; in expf (map recsplitf subthms) diff -r befdc10ebb42 -r 5568b16aa477 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Tue Jun 02 11:03:02 2015 +0200 +++ b/src/HOL/Tools/TFL/post.ML Tue Jun 02 13:55:43 2015 +0200 @@ -78,7 +78,7 @@ val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *) val cntxt = union (op aconv) cntxtl cntxtr in - Rules.GEN_ALL + Rules.GEN_ALL ctxt (Rules.DISCH_ALL (rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th))) end @@ -211,7 +211,8 @@ #1 (USyntax.strip_comb (#lhs (USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (USyntax.strip_imp tm))))))); fun defer_i congs fid eqs thy = - let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs + let + val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules)); val dummy = writeln "Proving induction theorem ..."; val induction = Prim.mk_induction theory diff -r befdc10ebb42 -r 5568b16aa477 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Tue Jun 02 11:03:02 2015 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Tue Jun 02 13:55:43 2015 +0200 @@ -21,22 +21,22 @@ val SPEC: cterm -> thm -> thm val ISPEC: cterm -> thm -> thm val ISPECL: cterm list -> thm -> thm - val GEN: cterm -> thm -> thm - val GENL: cterm list -> thm -> thm + val GEN: Proof.context -> cterm -> thm -> thm + val GENL: Proof.context -> cterm list -> thm -> thm val LIST_CONJ: thm list -> thm val SYM: thm -> thm val DISCH_ALL: thm -> thm val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm val SPEC_ALL: thm -> thm - val GEN_ALL: thm -> thm + val GEN_ALL: Proof.context -> thm -> thm val IMP_TRANS: thm -> thm -> thm val PROVE_HYP: thm -> thm -> thm val CHOOSE: Proof.context -> cterm * thm -> thm -> thm val EXISTS: cterm * cterm -> thm -> thm val EXISTL: cterm list -> thm -> thm - val IT_EXISTS: (cterm*cterm) list -> thm -> thm + val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm val EVEN_ORS: thm list -> thm list val DISJ_CASESL: thm -> thm list -> thm @@ -158,19 +158,19 @@ (*---------------------------------------------------------------------------- * Disjunction *---------------------------------------------------------------------------*) -local val thy = Thm.theory_of_thm disjI1 - val prop = Thm.prop_of disjI1 - val [P,Q] = Misc_Legacy.term_vars prop - val disj1 = Thm.forall_intr (Thm.global_cterm_of thy Q) disjI1 +local + val prop = Thm.prop_of disjI1 + val [P,Q] = Misc_Legacy.term_vars prop + val disj1 = Thm.forall_intr (Thm.cterm_of @{context} Q) disjI1 in fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1) handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg; end; -local val thy = Thm.theory_of_thm disjI2 - val prop = Thm.prop_of disjI2 - val [P,Q] = Misc_Legacy.term_vars prop - val disj2 = Thm.forall_intr (Thm.global_cterm_of thy P) disjI2 +local + val prop = Thm.prop_of disjI2 + val [P,Q] = Misc_Legacy.term_vars prop + val disj2 = Thm.forall_intr (Thm.cterm_of @{context} P) disjI2 in fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2) handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg; @@ -262,11 +262,10 @@ * Universals *---------------------------------------------------------------------------*) local (* this is fragile *) - val thy = Thm.theory_of_thm spec - val prop = Thm.prop_of spec - val x = hd (tl (Misc_Legacy.term_vars prop)) - val cTV = Thm.global_ctyp_of thy (type_of x) - val gspec = Thm.forall_intr (Thm.global_cterm_of thy x) spec + 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 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 @@ -279,41 +278,38 @@ val ISPECL = fold ISPEC; (* Not optimized! Too complicated. *) -local val thy = Thm.theory_of_thm allI - val prop = Thm.prop_of allI - val [P] = Misc_Legacy.add_term_vars (prop, []) - fun cty_theta s = map (fn (i, (S, ty)) => (Thm.global_ctyp_of s (TVar (i, S)), Thm.global_ctyp_of s ty)) - fun ctm_theta s = map (fn (i, (_, tm2)) => - let val ctm2 = Thm.global_cterm_of s tm2 - in (Thm.global_cterm_of s (Var(i, Thm.typ_of_cterm ctm2)), ctm2) - end) - fun certify s (ty_theta,tm_theta) = - (cty_theta s (Vartab.dest ty_theta), - ctm_theta s (Vartab.dest tm_theta)) +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 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) + fun certify ctxt (ty_theta,tm_theta) = + (cty_theta ctxt (Vartab.dest ty_theta), + ctm_theta ctxt (Vartab.dest tm_theta)) in -fun GEN v th = +fun GEN ctxt v th = let val gth = Thm.forall_intr v th - val thy = Thm.theory_of_thm gth + val thy = Proof_Context.theory_of ctxt val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty); - val allI2 = Drule.instantiate_normalize (certify thy theta) allI + val allI2 = Drule.instantiate_normalize (certify ctxt theta) allI val thm = Thm.implies_elim allI2 gth val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm val prop' = tp $ (A $ Abs(x,ty,M)) - in ALPHA thm (Thm.global_cterm_of thy prop') - end + in ALPHA thm (Thm.cterm_of ctxt prop') end end; -val GENL = fold_rev GEN; +fun GENL ctxt = fold_rev (GEN ctxt); -fun GEN_ALL thm = - let val thy = Thm.theory_of_thm thm - val prop = Thm.prop_of thm - val tycheck = Thm.global_cterm_of thy - val vlist = map tycheck (Misc_Legacy.add_term_vars (prop, [])) - in GENL vlist thm - end; +fun GEN_ALL ctxt thm = + let + val prop = Thm.prop_of thm + val vlist = map (Thm.cterm_of ctxt) (Misc_Legacy.add_term_vars (prop, [])) + in GENL ctxt vlist thm end; fun MATCH_MP th1 th2 = @@ -344,24 +340,19 @@ val t$u = Thm.term_of redex val residue = Thm.cterm_of ctxt (Term.betapply (t, u)) in - GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm) + GEN ctxt fvar (DISCH residue fact) RS (exth RS Thms.choose_thm) handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg end; -local val thy = Thm.theory_of_thm exI - val prop = Thm.prop_of exI - val [P,x] = Misc_Legacy.term_vars prop +local + val prop = Thm.prop_of exI + val [P, x] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars prop) in fun EXISTS (template,witness) thm = - let val thy = Thm.theory_of_thm thm - val prop = Thm.prop_of thm - val P' = Thm.global_cterm_of thy P - val x' = Thm.global_cterm_of thy x - val abstr = #2 (Dcterm.dest_comb template) - in - thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI) - handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg - end + let val abstr = #2 (Dcterm.dest_comb template) in + thm RS (cterm_instantiate [(P, abstr), (x, witness)] exI) + handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg + end end; (*---------------------------------------------------------------------------- @@ -386,16 +377,14 @@ *---------------------------------------------------------------------------*) (* Could be improved, but needs "subst_free" for certified terms *) -fun IT_EXISTS blist th = - let val thy = Thm.theory_of_thm th - val tych = Thm.global_cterm_of thy - val blist' = map (apply2 Thm.term_of) blist - fun ex v M = Thm.global_cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M}) - +fun IT_EXISTS ctxt blist th = + let + val blist' = map (apply2 Thm.term_of) blist + fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M}) in - fold_rev (fn (b as (r1,r2)) => fn thm => + fold_rev (fn (b as (r1,r2)) => fn thm => EXISTS(ex r2 (subst_free [b] - (HOLogic.dest_Trueprop(Thm.prop_of thm))), tych r1) + (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1) thm) blist' th end; @@ -509,13 +498,10 @@ (* Note: Thm.rename_params_rule counts from 1, not 0 *) fun rename thm = - let val thy = Thm.theory_of_thm thm - val tych = Thm.global_cterm_of thy - val ants = Logic.strip_imp_prems (Thm.prop_of thm) - val news = get (ants,1,[]) - in - fold Thm.rename_params_rule news thm - end; + let + val ants = Logic.strip_imp_prems (Thm.prop_of thm) + val news = get (ants,1,[]) + in fold Thm.rename_params_rule news thm end; (*--------------------------------------------------------------------------- @@ -737,10 +723,9 @@ handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *) fun restrict_prover ctxt thm = - let val dummy = say "restrict_prover:" + let val _ = say "restrict_prover:" val cntxt = rev (Simplifier.prems_of ctxt) - val dummy = print_thms ctxt "cntxt:" cntxt - val thy = Thm.theory_of_thm thm + val _ = print_thms ctxt "cntxt:" cntxt val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm fun genl tm = let val vlist = subtract (op aconv) globals @@ -762,14 +747,13 @@ val antl = case rcontext of [] => [] | _ => [USyntax.list_mk_conj(map cncl rcontext)] val TC = genl(USyntax.list_mk_imp(antl, A)) - val dummy = print_cterm ctxt "func:" (Thm.global_cterm_of thy func) - val dummy = print_cterm ctxt "TC:" (Thm.global_cterm_of thy (HOLogic.mk_Trueprop TC)) + val dummy = print_cterm ctxt "func:" (Thm.cterm_of ctxt func) + val dummy = print_cterm ctxt "TC:" (Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC)) val dummy = tc_list := (TC :: !tc_list) val nestedp = is_some (USyntax.find_term is_func TC) val dummy = if nestedp then say "nested" else say "not_nested" val th' = if nestedp then raise RULES_ERR "solver" "nested function" - else let val cTC = Thm.global_cterm_of thy - (HOLogic.mk_Trueprop TC) + else let val cTC = Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC) in case rcontext of [] => SPEC_ALL(ASSUME cTC) | _ => MP (SPEC_ALL (ASSUME cTC)) diff -r befdc10ebb42 -r 5568b16aa477 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Tue Jun 02 11:03:02 2015 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Tue Jun 02 13:55:43 2015 +0200 @@ -535,30 +535,30 @@ val (c,args) = USyntax.strip_comb lhs val (name,Ty) = dest_atom c val defn = const_def thy (name, Ty, USyntax.list_mk_abs (args,rhs)) - val ([def0], theory) = + val ([def0], thy') = thy |> Global_Theory.add_defs false [Thm.no_attributes (Binding.name (Thm.def_name fid), defn)] val def = Thm.unvarify_global def0; + val ctxt' = Syntax.init_pretty_global thy'; val dummy = - if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def) + if !trace then writeln ("DEF = " ^ Display.string_of_thm ctxt' def) else () (* val fconst = #lhs(USyntax.dest_eq(concl def)) *) - val tych = Thry.typecheck theory + val tych = Thry.typecheck thy' val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt (*lcp: a lot of object-logic inference to remove*) val baz = Rules.DISCH_ALL (fold_rev Rules.DISCH full_rqt_prop (Rules.LIST_CONJ extractants)) - val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz) - else () + val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm ctxt' baz) else () val f_free = Free (fid, fastype_of f) (*'cos f is a Const*) val SV' = map tych SV; val SVrefls = map Thm.reflexive SV' val def0 = (fold (fn x => fn th => Rules.rbeta(Thm.combination th x)) SVrefls def) RS meta_eq_to_obj_eq - val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN (tych R1) baz)) def0 + val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN ctxt' (tych R1) baz)) def0 val body_th = Rules.LIST_CONJ (map Rules.ASSUME full_rqt_prop) val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon theory Hilbert_Choice*) @@ -566,7 +566,7 @@ handle ERROR msg => cat_error msg "defer_recdef requires theory Main or at least Hilbert_Choice as parent" val bar = Rules.MP (Rules.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th - in {theory = theory, R=R1, SV=SV, + in {theory = thy', R=R1, SV=SV, rules = fold (fn a => fn b => Rules.MP b a) (Rules.CONJUNCTS bar) def', full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)), patterns = pats} @@ -633,7 +633,7 @@ fun fail s = raise TFL_ERR "mk_case" s fun mk{rows=[],...} = fail"no rows" | mk{path=[], rows = [([], (thm, bindings))]} = - Rules.IT_EXISTS (map tych_binding bindings) thm + Rules.IT_EXISTS ctxt (map tych_binding bindings) thm | mk{path = u::rstp, rows as (p::_, _)::_} = let val (pat_rectangle,rights) = ListPair.unzip rows val col0 = map hd pat_rectangle @@ -693,7 +693,7 @@ val th0 = Rules.ASSUME (tych a_eq_v) val rows = map (fn x => ([x], (th0,[]))) pats in - Rules.GEN (tych a) + Rules.GEN ctxt (tych a) (Rules.RIGHT_ASSOC ctxt (Rules.CHOOSE ctxt (tych v, ex_th0) (mk_case ty_info (vname::aname::names) @@ -774,14 +774,14 @@ * TCs = TC_1[pat] ... TC_n[pat] * thm = ih1 /\ ... /\ ih_n |- ih[pat] *---------------------------------------------------------------------------*) -fun prove_case f thy (tm,TCs_locals,thm) = - let val tych = Thry.typecheck thy +fun prove_case ctxt f (tm,TCs_locals,thm) = + let val tych = Thry.typecheck (Proof_Context.theory_of ctxt) val antc = tych(#ant(USyntax.dest_imp tm)) val thm' = Rules.SPEC_ALL thm fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm) fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC))))) fun mk_ih ((TC,locals),th2,nested) = - Rules.GENL (map tych locals) + Rules.GENL ctxt (map tych locals) (if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2 else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2 else Rules.MP th2 TC) @@ -845,7 +845,7 @@ val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums)) val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum) - val proved_cases = map (prove_case fconst thy) tasks + val proved_cases = map (prove_case ctxt fconst) tasks val v = Free (singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v", @@ -855,14 +855,14 @@ val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th') (substs, proved_cases) val abs_cases = map (LEFT_ABS_VSTRUCT ctxt tych) proved_cases1 - val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases) + val dant = Rules.GEN ctxt vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases) val dc = Rules.MP Sinduct dant val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc))) val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty) - val dc' = fold_rev (Rules.GEN o tych) vars + val dc' = fold_rev (Rules.GEN ctxt o tych) vars (Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc) in - Rules.GEN (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc') + Rules.GEN ctxt (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc') end handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation"; @@ -966,7 +966,7 @@ fun simplify_nested_tc tc = let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc))) in - Rules.GEN_ALL + Rules.GEN_ALL ctxt (Rules.MATCH_MP Thms.eqT tc_eq handle Utils.ERR _ => (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq) diff -r befdc10ebb42 -r 5568b16aa477 src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Tue Jun 02 11:03:02 2015 +0200 +++ b/src/HOL/Tools/split_rule.ML Tue Jun 02 13:55:43 2015 +0200 @@ -53,9 +53,8 @@ (incr_boundvars 1 u) $ Bound 0)) | ap_split' _ _ u = u; -fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) = +fun complete_split_rule_var ctxt (t as Var (v, T), ts) (rl, vs) = let - val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl) val (Us', U') = strip_type T; val Us = take (length ts) Us'; val U = drop (length ts) Us' ---> U'; @@ -64,17 +63,19 @@ let val Ts = HOLogic.flatten_tupleT T; val ys = Name.variant_list xs (replicate (length Ts) a); - in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T - (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts) + 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) end | mk_tuple _ x = x; val newt = ap_split' Us U (Var (v, T')); - val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl); val (vs', insts) = fold mk_tuple ts (vs, []); in - (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs') + (Drule.instantiate_normalize ([], [apply2 (Thm.cterm_of ctxt) (t, newt)] @ insts) rl, vs') end - | complete_split_rule_var _ x = x; + | complete_split_rule_var _ _ x = x; fun collect_vars (Abs (_, _, t)) = collect_vars t | collect_vars t = @@ -99,7 +100,7 @@ val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop []; val vars = collect_vars prop []; in - fst (fold_rev complete_split_rule_var vars (rl, xs)) + fst (fold_rev (complete_split_rule_var ctxt) vars (rl, xs)) |> remove_internal_split ctxt |> Drule.export_without_context |> Rule_Cases.save rl