1.1 --- a/src/HOL/Statespace/state_fun.ML	Sun Mar 28 15:38:07 2010 +0200
     1.2 +++ b/src/HOL/Statespace/state_fun.ML	Sun Mar 28 16:29:51 2010 +0200
     1.3 @@ -142,7 +142,7 @@
     1.4            val ctxt = Simplifier.the_context ss;
     1.5            val basic_ss = #1 (StateFunData.get (Context.Proof ctxt));
     1.6            val ss' = Simplifier.context 
     1.7 -                     (Config.map MetaSimplifier.simp_depth_limit (K 100) ctxt) basic_ss;
     1.8 +                     (Config.put MetaSimplifier.simp_depth_limit 100 ctxt) basic_ss;
     1.9            val thm = Simplifier.rewrite ss' ct;
    1.10          in if (op aconv) (Logic.dest_equals (prop_of thm))
    1.11             then NONE
    1.12 @@ -233,7 +233,7 @@
    1.13                 | mk_updterm _ t = init_seed t;
    1.14  
    1.15               val ctxt = Simplifier.the_context ss |>
    1.16 -                        Config.map MetaSimplifier.simp_depth_limit (K 100);
    1.17 +                        Config.put MetaSimplifier.simp_depth_limit 100;
    1.18               val ss1 = Simplifier.context ctxt ss';
    1.19               val ss2 = Simplifier.context ctxt 
    1.20                           (#1 (StateFunData.get (Context.Proof ctxt)));
    1.21 @@ -267,7 +267,7 @@
    1.22      (fn thy => fn ss => fn t =>
    1.23         let
    1.24           val ctxt = Simplifier.the_context ss |>
    1.25 -                    Config.map MetaSimplifier.simp_depth_limit (K 100)
    1.26 +                    Config.put MetaSimplifier.simp_depth_limit 100
    1.27           val ex_lookup_ss = #2 (StateFunData.get (Context.Proof ctxt));
    1.28           val ss' = (Simplifier.context ctxt ex_lookup_ss);
    1.29           fun prove prop =