# HG changeset patch
# User wenzelm
# Date 1269786591 -7200
# Node ID e031755609cffa9b0ad9f2f38fdf40c99f967e4a
# Parent  6b8f789554ae9423bb001640d564178c107ee81b
tuned;

diff -r 6b8f789554ae -r e031755609cf src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Sun Mar 28 15:38:07 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Sun Mar 28 16:29:51 2010 +0200
@@ -142,7 +142,7 @@
           val ctxt = Simplifier.the_context ss;
           val basic_ss = #1 (StateFunData.get (Context.Proof ctxt));
           val ss' = Simplifier.context 
-                     (Config.map MetaSimplifier.simp_depth_limit (K 100) ctxt) basic_ss;
+                     (Config.put MetaSimplifier.simp_depth_limit 100 ctxt) basic_ss;
           val thm = Simplifier.rewrite ss' ct;
         in if (op aconv) (Logic.dest_equals (prop_of thm))
            then NONE
@@ -233,7 +233,7 @@
                | mk_updterm _ t = init_seed t;
 
              val ctxt = Simplifier.the_context ss |>
-                        Config.map MetaSimplifier.simp_depth_limit (K 100);
+                        Config.put MetaSimplifier.simp_depth_limit 100;
              val ss1 = Simplifier.context ctxt ss';
              val ss2 = Simplifier.context ctxt 
                          (#1 (StateFunData.get (Context.Proof ctxt)));
@@ -267,7 +267,7 @@
     (fn thy => fn ss => fn t =>
        let
          val ctxt = Simplifier.the_context ss |>
-                    Config.map MetaSimplifier.simp_depth_limit (K 100)
+                    Config.put MetaSimplifier.simp_depth_limit 100
          val ex_lookup_ss = #2 (StateFunData.get (Context.Proof ctxt));
          val ss' = (Simplifier.context ctxt ex_lookup_ss);
          fun prove prop =