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:
authorwenzelm
Mon Feb 10 13:04:08 2014 +0100 (2014-02-10)
changeset 55377d79c057c68f0
parent 55374 636a8523876f
child 55378 e61e023c9faf
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
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Sun Feb 09 21:37:27 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Mon Feb 10 13:04:08 2014 +0100
     1.3 @@ -375,11 +375,7 @@
     1.4  
     1.5  fun simpset_map ctxt f ss = ctxt |> map_simpset (K ss) |> f |> Context.Proof |> Simpset.get;
     1.6  
     1.7 -fun put_simpset ss = map_simpset (fn context_ss =>
     1.8 -  let
     1.9 -    val Simpset ({rules, prems, ...}, ss2) = ss;  (* FIXME prems from context (!?) *)
    1.10 -    val Simpset ({depth, ...}, _) = context_ss;
    1.11 -  in Simpset (make_ss1 (rules, prems, depth), ss2) end);
    1.12 +fun put_simpset ss = map_simpset (K ss);
    1.13  
    1.14  val empty_simpset = put_simpset empty_ss;
    1.15