--- 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;