src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML

     ^ "\n" ^ Pretty.string_of (Pretty.chunks
       (Goal_Display.pretty_goals_without_context st)));
 
 
 (** special setup for simpset **)
-val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
+val HOL_basic_ss' = HOL_basic_ss addsimps @{thms simp_thms Pair_eq}
   setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
   setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
 
 (* auxillary functions *)
 

       (fn (pred, T) => predfun_definition_of ctxt pred
         (all_input_of T))
         preds
   in 
     simp_tac (HOL_basic_ss addsimps
-      (@{thms HOL.simp_thms} @ (@{thm eval_pred} :: defs))) 1 
+      (@{thms HOL.simp_thms eval_pred} @ defs)) 1 
     (* need better control here! *)
   end
 
 fun prove_clause options ctxt nargs mode (_, clauses) (ts, moded_ps) =
   let