src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML

     val param_derivations = param_derivations_of deriv
     val ho_args = ho_args_of mode args
     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 _ =>
         Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} =>
           let

       (fn (pred, T) => Core_Data.predfun_definition_of ctxt pred
         (all_input_of T))
         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
 
 fun prove_clause options ctxt nargs mode (_, clauses) (ts, moded_ps) =
   let

     val param_derivations = param_derivations_of deriv
     val ho_args = ho_args_of mode args
     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")
   in
     trace_tac ctxt options "before simplification in prove_args:"

       (fn (pred, T) => Core_Data.predfun_definition_of ctxt pred
         (all_input_of T))
         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
 
 fun prove_clause2 options ctxt pred mode (ts, ps) i =