more elementary put_simpset: exchange the simplifier configuration outright, which is particularly relevant concerning cumulative depth, e.g. for Product_Type.split_beta in the subsequent example:

lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))"
using [[simp_depth_limit = 1]]
apply simp
oops

--- a/src/Pure/raw_simplifier.ML	Sun Feb 09 21:37:27 2014 +0100
+++ b/src/Pure/raw_simplifier.ML	Mon Feb 10 13:04:08 2014 +0100
@@ -375,11 +375,7 @@
 
 fun simpset_map ctxt f ss = ctxt |> map_simpset (K ss) |> f |> Context.Proof |> Simpset.get;
 
-fun put_simpset ss = map_simpset (fn context_ss =>
-  let
-    val Simpset ({rules, prems, ...}, ss2) = ss;  (* FIXME prems from context (!?) *)
-    val Simpset ({depth, ...}, _) = context_ss;
-  in Simpset (make_ss1 (rules, prems, depth), ss2) end);
+fun put_simpset ss = map_simpset (K ss);
 
 val empty_simpset = put_simpset empty_ss;