--- 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 [] \<bullet> 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
--- 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. *)
--- 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)) =
--- 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);
--- 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 \<Rightarrow> nat \<Rightarrow> 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)) =
--- 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 ^
--- 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),
--- 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);
--- 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';
--- 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;