--- a/src/HOL/Statespace/state_fun.ML Fri Dec 17 14:09:37 2010 +0100
+++ b/src/HOL/Statespace/state_fun.ML Fri Dec 17 16:25:21 2010 +0100
@@ -141,8 +141,7 @@
(Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s)));
val ctxt = Simplifier.the_context ss;
val basic_ss = #1 (StateFunData.get (Context.Proof ctxt));
- val ss' = Simplifier.context
- (Config.put MetaSimplifier.simp_depth_limit 100 ctxt) basic_ss;
+ val ss' = Simplifier.context (Config.put 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
@@ -232,8 +231,7 @@
end
| mk_updterm _ t = init_seed t;
- val ctxt = Simplifier.the_context ss |>
- Config.put MetaSimplifier.simp_depth_limit 100;
+ val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100;
val ss1 = Simplifier.context ctxt ss';
val ss2 = Simplifier.context ctxt
(#1 (StateFunData.get (Context.Proof ctxt)));
@@ -266,8 +264,7 @@
Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
(fn thy => fn ss => fn t =>
let
- val ctxt = Simplifier.the_context ss |>
- Config.put MetaSimplifier.simp_depth_limit 100
+ val ctxt = Simplifier.the_context ss |> Config.put 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 =