--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Mon Jun 05 15:59:45 2017 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Mon Jun 05 15:59:45 2017 +0200
@@ -61,7 +61,7 @@
val f_tac =
(case f of
Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
- [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode,
+ [@{thm pred.sel}, Core_Data.predfun_definition_of ctxt name mode,
@{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv},
@{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1
| Free _ =>
@@ -180,7 +180,7 @@
preds
in
simp_tac (put_simpset HOL_basic_ss ctxt
- addsimps (@{thms HOL.simp_thms eval_pred} @ defs)) 1
+ addsimps (@{thms HOL.simp_thms pred.sel} @ defs)) 1
(* need better control here! *)
end
@@ -339,7 +339,7 @@
val f_tac =
(case f of
Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
- [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode,
+ [@{thm pred.sel}, Core_Data.predfun_definition_of ctxt name mode,
@{thm Product_Type.split_conv}]) 1
| Free _ => all_tac
| _ => error "prove_param2: illegal parameter term")
@@ -383,7 +383,7 @@
preds
in
(* only simplify the one assumption *)
- full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1
+ full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm pred.sel} :: defs) 1
(* need better control here! *)
THEN trace_tac ctxt options "after sidecond2 simplification"
end