1.1 --- a/src/Tools/isac/Interpret/derive.sml	Thu Nov 10 14:25:38 2022 +0100
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Wed Nov 16 10:29:52 2022 +0100
     1.3 @@ -53,11 +53,11 @@
     1.4  fun msg_2 ctxt thmid =
     1.5    if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
     1.6  fun msg_3 ctxt t' =
     1.7 -  if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
     1.8 +  if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term_in_ctxt ctxt t') else ();
     1.9  fun msg_4 ctxt op_ =
    1.10    if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying calc. \"" ^ op_^"\"");
    1.11  fun msg_5 ctxt t' =
    1.12 -  if not (Config.get ctxt rewrite_trace) then () else tracing("=== calc. to: " ^ UnparseC.term t')
    1.13 +  if not (Config.get ctxt rewrite_trace) then () else tracing("=== calc. to: " ^ UnparseC.term_in_ctxt ctxt t')
    1.14  
    1.15  
    1.16  fun do_one ctxt asm_rls rs ro goal tt = 
    1.17 @@ -65,7 +65,7 @@
    1.18      datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *)
    1.19      fun rew_once _ rts t Noap [] = 
    1.20          (case goal of NONE => rts | SOME _ =>
    1.21 -          raise ERROR ("Derive.do_one: no derivation for " ^ UnparseC.term t))
    1.22 +          raise ERROR ("Derive.do_one: no derivation for " ^ UnparseC.term_in_ctxt ctxt t))
    1.23        | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
    1.24        | rew_once lim rts t apno rs' =
    1.25          (case goal of