1.1 --- a/src/Tools/isac/Interpret/derive.sml	Sat Jul 30 16:47:45 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Sun Jul 31 12:39:07 2022 +0200
     1.3 @@ -47,8 +47,8 @@
     1.4  
     1.5  (** make one triple towards the goal term **)
     1.6  
     1.7 -fun msg_1 rts =
     1.8 -  (tracing ("do_one exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with derivation =\n");
     1.9 +fun msg_1 ctxt rts =
    1.10 +  (tracing ("do_one exceeds " ^ int2str (Config.get ctxt rewrite_limit) ^ "with derivation =\n");
    1.11     tracing (deriv2str rts));
    1.12  fun msg_2 ctxt thmid =
    1.13    if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
    1.14 @@ -73,7 +73,7 @@
    1.15          | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
    1.16      and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
    1.17        if lim < 0 
    1.18 -      then (msg_1 rts; rts)
    1.19 +      then (msg_1 ctxt rts; rts)
    1.20        else
    1.21          (case r of
    1.22            Rule.Thm (thmid, tm) => 
    1.23 @@ -101,7 +101,7 @@
    1.24            | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
    1.25          | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule))
    1.26      | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []"
    1.27 -  in rew_once (! Rewrite.lim_deriv) [] tt Noap rs end
    1.28 +  in rew_once (Config.get ctxt rewrite_limit) [] tt Noap rs end
    1.29  
    1.30  
    1.31  (** concatenate several steps in revers order **)