# HG changeset patch # User wenzelm # Date 1433158516 -7200 # Node ID 9c94e6a30d29404d4a7d33239c1021a8a4ec13c6 # Parent a3f565b8ba767d2fd9e915f2c1ff5e3c706d9f99 clarified context; diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Mon Jun 01 13:32:36 2015 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Mon Jun 01 13:35:16 2015 +0200 @@ -281,8 +281,9 @@ Const (@{const_name Nominal.perm}, T) $ pi $ Free (x, T2)) end) (perm_names_types ~~ perm_indnames)))) - (fn {context = ctxt, ...} => EVERY [Old_Datatype_Aux.ind_tac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac (ctxt addsimps [perm_fun_def]))])), + (fn {context = ctxt, ...} => + EVERY [Old_Datatype_Aux.ind_tac ctxt induct perm_indnames 1, + ALLGOALS (asm_full_simp_tac (ctxt addsimps [perm_fun_def]))])), length new_type_names)); (**** prove [] \ t = t ****) @@ -301,8 +302,9 @@ Free (x, T))) (perm_names ~~ map body_type perm_types ~~ perm_indnames))))) - (fn {context = ctxt, ...} => EVERY [Old_Datatype_Aux.ind_tac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac ctxt)])), + (fn {context = ctxt, ...} => + EVERY [Old_Datatype_Aux.ind_tac ctxt induct perm_indnames 1, + ALLGOALS (asm_full_simp_tac ctxt)])), length new_type_names)) end) atoms; @@ -336,8 +338,9 @@ end) (perm_names ~~ map body_type perm_types ~~ perm_indnames))))) - (fn {context = ctxt, ...} => EVERY [Old_Datatype_Aux.ind_tac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac (ctxt addsimps [pt2', pt2_ax]))]))), + (fn {context = ctxt, ...} => + EVERY [Old_Datatype_Aux.ind_tac ctxt induct perm_indnames 1, + ALLGOALS (asm_full_simp_tac (ctxt addsimps [pt2', pt2_ax]))]))), length new_type_names) end) atoms; @@ -372,8 +375,9 @@ end) (perm_names ~~ map body_type perm_types ~~ perm_indnames)))))) - (fn {context = ctxt, ...} => EVERY [Old_Datatype_Aux.ind_tac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac (ctxt addsimps [pt3', pt3_rev', pt3_ax]))]))), + (fn {context = ctxt, ...} => + EVERY [Old_Datatype_Aux.ind_tac ctxt induct perm_indnames 1, + ALLGOALS (asm_full_simp_tac (ctxt addsimps [pt3', pt3_rev', pt3_ax]))]))), length new_type_names) end) atoms; @@ -424,8 +428,9 @@ perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T))) end) (perm_names ~~ Ts ~~ perm_indnames))))) - (fn {context = ctxt, ...} => EVERY [Old_Datatype_Aux.ind_tac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac (simps ctxt))])) + (fn {context = ctxt, ...} => + EVERY [Old_Datatype_Aux.ind_tac ctxt induct perm_indnames 1, + ALLGOALS (asm_full_simp_tac (simps ctxt))])) in fold (fn (s, tvs) => fn thy => Axclass.prove_arity (s, map (inter_sort thy sort o snd) tvs, [cp_class]) @@ -562,7 +567,7 @@ Free ("pi", permT) $ Free (x, T))) end) (rep_set_names'' ~~ recTs' ~~ perm_indnames'))))) (fn {context = ctxt, ...} => EVERY - [Old_Datatype_Aux.ind_tac rep_induct [] 1, + [Old_Datatype_Aux.ind_tac ctxt rep_induct [] 1, ALLGOALS (simp_tac (ctxt addsimps (Thm.symmetric perm_fun_def :: abs_perm))), ALLGOALS (resolve_tac ctxt rep_intrs THEN_ALL_NEW assume_tac ctxt)])), @@ -1060,7 +1065,8 @@ (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop) (fn {prems, context = ctxt} => EVERY [rtac indrule_lemma' 1, - (Old_Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1, + (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW + Object_Logic.atomize_prems_tac ctxt) 1, EVERY (map (fn (prem, r) => (EVERY [REPEAT (eresolve_tac ctxt Abs_inverse_thms' 1), simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1, @@ -1089,8 +1095,9 @@ Const (@{const_name finite}, HOLogic.mk_setT atomT --> HOLogic.boolT) $ (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT atomT) $ Free (s, T))) (indnames ~~ recTs))))) - (fn {context = ctxt, ...} => Old_Datatype_Aux.ind_tac dt_induct indnames 1 THEN - ALLGOALS (asm_full_simp_tac (ctxt addsimps + (fn {context = ctxt, ...} => + Old_Datatype_Aux.ind_tac ctxt dt_induct indnames 1 THEN + ALLGOALS (asm_full_simp_tac (ctxt addsimps (abs_supp @ supp_atm @ Global_Theory.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @ flat supp_thms))))), @@ -1308,7 +1315,7 @@ val th = Goal.prove context [] [] (augment_sort thy9 fs_cp_sort aux_ind_concl) (fn {context = context1, ...} => - EVERY (Old_Datatype_Aux.ind_tac dt_induct tnames 1 :: + EVERY (Old_Datatype_Aux.ind_tac context1 dt_induct tnames 1 :: maps (fn ((_, (_, _, constrs)), (_, constrs')) => map (fn ((cname, cargs), is) => REPEAT (rtac allI 1) THEN diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jun 01 13:32:36 2015 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jun 01 13:35:16 2015 +0200 @@ -759,7 +759,7 @@ fun do_introduce_combinators ctxt Ts t = (t |> conceal_bounds Ts |> Thm.cterm_of ctxt - |> Meson_Clausify.introduce_combinators_in_cterm + |> Meson_Clausify.introduce_combinators_in_cterm ctxt |> Thm.prop_of |> Logic.dest_equals |> snd |> reveal_bounds Ts) (* A type variable of sort "{}" will make abstraction fail. *) diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Mon Jun 01 13:32:36 2015 +0200 +++ b/src/HOL/Tools/Function/function_lib.ML Mon Jun 01 13:35:16 2015 +0200 @@ -18,7 +18,7 @@ val forall_intr_rename: (string * cterm) -> thm -> thm datatype proof_attempt = Solved of thm | Stuck of thm | Fail - val try_proof: cterm -> tactic -> proof_attempt + val try_proof: Proof.context -> cterm -> tactic -> proof_attempt val dest_binop_list: string -> term -> term list val regroup_conv: Proof.context -> string -> string -> thm list -> int list -> conv @@ -68,13 +68,13 @@ datatype proof_attempt = Solved of thm | Stuck of thm | Fail -fun try_proof cgoal tac = - case SINGLE tac (Goal.init cgoal) of +fun try_proof ctxt cgoal tac = + (case SINGLE tac (Goal.init cgoal) of NONE => Fail | SOME st => - if Thm.no_prems st - then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st) - else Stuck st + if Thm.no_prems st + then Solved (Goal.finish ctxt st) + else Stuck st) fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Mon Jun 01 13:32:36 2015 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon Jun 01 13:35:16 2015 +0200 @@ -70,16 +70,16 @@ let val goals = Thm.cterm_of ctxt o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) in - case try_proof (goals @{const_name Orderings.less}) solve_tac of + (case try_proof ctxt (goals @{const_name Orderings.less}) solve_tac of Solved thm => Less thm | Stuck thm => - (case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of - Solved thm2 => LessEq (thm2, thm) - | Stuck thm2 => - if Thm.prems_of thm2 = [HOLogic.Trueprop $ @{term False}] then False thm2 - else None (thm2, thm) - | _ => raise Match) (* FIXME *) - | _ => raise Match + (case try_proof ctxt (goals @{const_name Orderings.less_eq}) solve_tac of + Solved thm2 => LessEq (thm2, thm) + | Stuck thm2 => + if Thm.prems_of thm2 = [HOLogic.Trueprop $ @{term False}] then False thm2 + else None (thm2, thm) + | _ => raise Match) (* FIXME *) + | _ => raise Match) end); diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Mon Jun 01 13:32:36 2015 +0200 +++ b/src/HOL/Tools/Function/termination.ML Mon Jun 01 13:35:16 2015 +0200 @@ -142,9 +142,9 @@ Const (@{const_abbrev Set.empty}, fastype_of c1)) |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *) in - case Function_Lib.try_proof (Thm.cterm_of ctxt goal) chain_tac of + (case Function_Lib.try_proof ctxt (Thm.cterm_of ctxt goal) chain_tac of Function_Lib.Solved thm => SOME thm - | _ => NONE + | _ => NONE) end @@ -167,22 +167,22 @@ fun mk_desc ctxt tac vs Gam l r m1 m2 = let fun try rel = - try_proof (Thm.cterm_of ctxt + try_proof ctxt (Thm.cterm_of ctxt (Logic.list_all (vs, Logic.mk_implies (HOLogic.mk_Trueprop Gam, - HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"}) + HOLogic.mk_Trueprop (Const (rel, @{typ "nat \ nat \ bool"}) $ (m2 $ r) $ (m1 $ l)))))) tac in - case try @{const_name Orderings.less} of - Solved thm => Less thm - | Stuck thm => - (case try @{const_name Orderings.less_eq} of + (case try @{const_name Orderings.less} of + Solved thm => Less thm + | Stuck thm => + (case try @{const_name Orderings.less_eq} of Solved thm2 => LessEq (thm2, thm) | Stuck thm2 => - if Thm.prems_of thm2 = [HOLogic.Trueprop $ @{term False}] - then False thm2 else None (thm2, thm) + if Thm.prems_of thm2 = [HOLogic.Trueprop $ @{term False}] + then False thm2 else None (thm2, thm) | _ => raise Match) (* FIXME *) - | _ => raise Match + | _ => raise Match) end fun prove_descent ctxt tac sk (c, (m1, m2)) = diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Mon Jun 01 13:32:36 2015 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Jun 01 13:35:16 2015 +0200 @@ -11,7 +11,7 @@ val new_nonskolem_var_prefix : string val is_zapped_var_name : string -> bool val is_quasi_lambda_free : term -> bool - val introduce_combinators_in_cterm : cterm -> thm + val introduce_combinators_in_cterm : Proof.context -> cterm -> thm val introduce_combinators_in_theorem : Proof.context -> thm -> thm val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool val ss_only : thm list -> Proof.context -> Proof.context @@ -99,16 +99,14 @@ val [f_S,g_S] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_S})); (* FIXME: Requires more use of cterm constructors. *) -fun abstract ct = +fun abstract ctxt ct = let - val thy = Thm.theory_of_cterm ct val Abs(x,_,body) = Thm.term_of ct val Type (@{type_name fun}, [xT,bodyT]) = Thm.typ_of_cterm ct - val cxT = Thm.global_ctyp_of thy xT - val cbodyT = Thm.global_ctyp_of thy bodyT + val cxT = Thm.ctyp_of ctxt xT + val cbodyT = Thm.ctyp_of ctxt bodyT fun makeK () = - instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.global_cterm_of thy body)] - @{thm abs_K} + instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.cterm_of ctxt body)] @{thm abs_K} in case body of Const _ => makeK() @@ -118,35 +116,35 @@ | rator$rand => if Term.is_dependent rator then (*C or S*) if Term.is_dependent rand then (*S*) - let val crator = Thm.global_cterm_of thy (Abs(x,xT,rator)) - val crand = Thm.global_cterm_of thy (Abs(x,xT,rand)) + let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator)) + val crand = Thm.cterm_of ctxt (Abs (x, xT, rand)) val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S} val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_S') in - Thm.transitive abs_S' (Conv.binop_conv abstract rhs) + Thm.transitive abs_S' (Conv.binop_conv (abstract ctxt) rhs) end else (*C*) - let val crator = Thm.global_cterm_of thy (Abs(x,xT,rator)) + let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator)) val abs_C' = - cterm_instantiate [(f_C,crator),(g_C,Thm.global_cterm_of thy rand)] @{thm abs_C} + cterm_instantiate [(f_C, crator), (g_C, Thm.cterm_of ctxt rand)] @{thm abs_C} val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_C') in - Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) + Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv (abstract ctxt)) rhs) end else if Term.is_dependent rand then (*B or eta*) if rand = Bound 0 then Thm.eta_conversion ct else (*B*) - let val crand = Thm.global_cterm_of thy (Abs(x,xT,rand)) - val crator = Thm.global_cterm_of thy rator + let val crand = Thm.cterm_of ctxt (Abs (x, xT, rand)) + val crator = Thm.cterm_of ctxt rator val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_B') - in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end - else makeK() + in Thm.transitive abs_B' (Conv.arg_conv (abstract ctxt) rhs) end + else makeK () | _ => raise Fail "abstract: Bad term" end; (* Traverse a theorem, remplacing lambda-abstractions with combinators. *) -fun introduce_combinators_in_cterm ct = +fun introduce_combinators_in_cterm ctxt ct = if is_quasi_lambda_free (Thm.term_of ct) then Thm.reflexive ct else case Thm.term_of ct of @@ -154,14 +152,14 @@ let val (cv, cta) = Thm.dest_abs NONE ct val (v, _) = dest_Free (Thm.term_of cv) - val u_th = introduce_combinators_in_cterm cta + val u_th = introduce_combinators_in_cterm ctxt cta val cu = Thm.rhs_of u_th - val comb_eq = abstract (Thm.lambda cv cu) + val comb_eq = abstract ctxt (Thm.lambda cv cu) in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end | _ $ _ => let val (ct1, ct2) = Thm.dest_comb ct in - Thm.combination (introduce_combinators_in_cterm ct1) - (introduce_combinators_in_cterm ct2) + Thm.combination (introduce_combinators_in_cterm ctxt ct1) + (introduce_combinators_in_cterm ctxt ct2) end fun introduce_combinators_in_theorem ctxt th = @@ -170,7 +168,7 @@ else let val th = Drule.eta_contraction_rule th - val eqth = introduce_combinators_in_cterm (Thm.cprop_of th) + val eqth = introduce_combinators_in_cterm ctxt (Thm.cprop_of th) in Thm.equal_elim eqth th end handle THM (msg, _, _) => (warning ("Error in the combinator translation of " ^ Display.string_of_thm ctxt th ^ diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Tools/Old_Datatype/old_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Jun 01 13:32:36 2015 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Jun 01 13:35:16 2015 +0200 @@ -418,7 +418,8 @@ Goal.prove_sorry_global thy5 [] [] (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj ind_concl1)) (fn {context = ctxt, ...} => EVERY - [(Old_Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1, + [(Old_Datatype_Aux.ind_tac ctxt induct [] THEN_ALL_NEW + Object_Logic.atomize_prems_tac ctxt) 1, REPEAT (EVERY [rtac allI 1, rtac impI 1, Old_Datatype_Aux.exh_tac ctxt (exh_thm_of dt_info) 1, @@ -445,7 +446,8 @@ (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj ind_concl2)) (fn {context = ctxt, ...} => EVERY [ - (Old_Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1, + (Old_Datatype_Aux.ind_tac ctxt induct [] THEN_ALL_NEW + Object_Logic.atomize_prems_tac ctxt) 1, rewrite_goals_tac ctxt rewrites, REPEAT ((resolve_tac ctxt rep_intrs THEN_ALL_NEW ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]); @@ -481,7 +483,7 @@ else drop (length newTs) (Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy5 [] [] iso_t (fn {context = ctxt, ...} => EVERY - [(Old_Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW + [(Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1, REPEAT (rtac TrueI 1), rewrite_goals_tac ctxt (mk_meta_eq @{thm choice_eq} :: @@ -636,7 +638,7 @@ (fn {context = ctxt, prems, ...} => EVERY [rtac indrule_lemma' 1, - (Old_Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW + (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1, EVERY (map (fn (prem, r) => (EVERY [REPEAT (eresolve_tac ctxt Abs_inverse_thms 1), diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Tools/Old_Datatype/old_datatype_aux.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Mon Jun 01 13:32:36 2015 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Mon Jun 01 13:35:16 2015 +0200 @@ -52,7 +52,7 @@ val app_bnds : term -> int -> term - val ind_tac : thm -> string list -> int -> tactic + val ind_tac : Proof.context -> thm -> string list -> int -> tactic val exh_tac : Proof.context -> (string -> thm) -> int -> tactic exception Datatype @@ -124,9 +124,8 @@ (* instantiate induction rule *) -fun ind_tac indrule indnames = CSUBGOAL (fn (cgoal, i) => +fun ind_tac ctxt indrule indnames = CSUBGOAL (fn (cgoal, i) => let - val thy = Thm.theory_of_cterm cgoal; val goal = Thm.term_of cgoal; val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule)); val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop (Logic.strip_imp_concl goal)); @@ -145,11 +144,10 @@ | _ => NONE) | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2)))); val insts = - map_filter (fn (t, u) => + (ts ~~ ts') |> map_filter (fn (t, u) => (case abstr (getP u) of NONE => NONE - | SOME u' => - SOME (apply2 (Thm.global_cterm_of thy) (t |> getP |> snd |> head_of, u')))) (ts ~~ ts'); + | SOME u' => SOME (apply2 (Thm.cterm_of ctxt) (t |> getP |> snd |> head_of, u')))); val indrule' = cterm_instantiate insts indrule; in resolve0_tac [indrule'] i end); diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Tools/Old_Datatype/old_size.ML --- a/src/HOL/Tools/Old_Datatype/old_size.ML Mon Jun 01 13:32:36 2015 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_size.ML Mon Jun 01 13:35:16 2015 +0200 @@ -152,7 +152,7 @@ map (mk_unfolded_size_eq (AList.lookup op = (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs) (xs ~~ recTs2 ~~ rec_combs2)))) - (fn _ => (Old_Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); + (fn _ => (Old_Datatype_Aux.ind_tac ctxt induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs; val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs'; diff -r a3f565b8ba76 -r 9c94e6a30d29 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Mon Jun 01 13:32:36 2015 +0200 +++ b/src/HOL/Tools/inductive_set.ML Mon Jun 01 13:35:16 2015 +0200 @@ -112,11 +112,10 @@ | eta b t = t in eta false end; -fun eta_contract_thm p = +fun eta_contract_thm ctxt p = Conv.fconv_rule (Conv.then_conv (Thm.beta_conversion true, fn ct => Thm.transitive (Thm.eta_conversion ct) - (Thm.symmetric (Thm.eta_conversion - (Thm.global_cterm_of (Thm.theory_of_cterm ct) (eta_contract p (Thm.term_of ct))))))); + (Thm.symmetric (Thm.eta_conversion (Thm.cterm_of ctxt (eta_contract p (Thm.term_of ct))))))); (***********************************************************) @@ -238,7 +237,7 @@ in Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [@{simproc Collect_mem}]) thm'' |> - zero_var_indexes |> eta_contract_thm (equal p) + zero_var_indexes |> eta_contract_thm ctxt (equal p) end; @@ -342,7 +341,7 @@ Thm.instantiate ([], insts) |> Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |> - eta_contract_thm (is_pred pred_arities) |> + eta_contract_thm ctxt (is_pred pred_arities) |> Rule_Cases.save thm end; @@ -402,7 +401,7 @@ thm |> Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |> - eta_contract_thm (is_pred pred_arities) + eta_contract_thm ctxt (is_pred pred_arities) else thm in map preproc end;