# HG changeset patch
# User wenzelm
# Date 1392033848 -3600
# Node ID d79c057c68f07912a404c6686cf0ea9fa0840be3
# Parent  636a8523876f2c02352b20aba2352ce8a97585f5
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

diff -r 636a8523876f -r d79c057c68f0 src/Pure/raw_simplifier.ML
--- 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;