1.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Sat Dec 03 19:12:38 2022 +0100
     1.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Sun Dec 04 16:48:06 2022 +0100
     1.3 @@ -288,7 +288,7 @@
     1.4  
     1.5  (*//--------------------- check results from modified me ----------------------------------\\*)
     1.6  if p = ([2], Res) andalso
     1.7 -  pr_ctree pr_short pt = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 = 2\n"
     1.8 +  pr_ctree ctxt pr_short pt = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 = 2\n"
     1.9  then
    1.10    (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
    1.11     | _ => error "")
    1.12 @@ -315,7 +315,7 @@
    1.13  (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
    1.14  
    1.15  (*/--------------------- final test ----------------------------------\\*)
    1.16 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
    1.17 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree ctxt pr_short pt =
    1.18    ".    ----- pblobj -----\n" ^
    1.19    "1.   x + 1 = 2\n" ^
    1.20    "2.   x + 1 + - 1 * 2 = 0\n" ^
    1.21 @@ -578,7 +578,7 @@
    1.22  val (res, asm) = (get_obj g_result pt (fst p));
    1.23  if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
    1.24  andalso p = ([], Und) andalso msg = "end-of-calculation"
    1.25 -andalso pr_ctree pr_short pt = ".    ----- pblobj -----\n1.   a + a\n"
    1.26 +andalso pr_ctree ctxt pr_short pt = ".    ----- pblobj -----\n1.   a + a\n"
    1.27  then 
    1.28    case tac''''' of Check_Postcond ["polynomial", "simplification"] => () 
    1.29    | _ => error "re-build: fun find_next_step, mini 1"
    1.30 @@ -690,7 +690,7 @@
    1.31   (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
    1.32  
    1.33  (*/--- final test ---------------------------------------------------------------------------\\*)
    1.34 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
    1.35 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree ctxt pr_short pt =
    1.36     ".    ----- pblobj -----\n" ^
    1.37     "1.   x + 1 = 2\n" ^
    1.38     "2.   x + 1 + - 1 * 2 = 0\n" ^