1.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Fri Apr 10 16:16:09 2020 +0200
     1.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Fri Apr 10 18:32:36 2020 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4  "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
     1.5    = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
     1.6  
     1.7 -(*+*) if UnparseC.term2str e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
     1.8 +(*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
     1.9  
    1.10      (*case*)
    1.11             scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
    1.12 @@ -333,11 +333,11 @@
    1.13    "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], empty, SOME t_t, \n" ^
    1.14    "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, ORundef, true, false)"
    1.15  andalso
    1.16 -  UnparseC.term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
    1.17 +  UnparseC.term t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
    1.18  andalso
    1.19 -  UnparseC.term2str res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g"
    1.20 +  UnparseC.term res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g"
    1.21  andalso
    1.22 -  UnparseC.terms2str asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"
    1.23 +  UnparseC.terms asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"
    1.24  then () else error "locate_input_tactic Helpless, but applicable CHANGED";
    1.25  
    1.26  
    1.27 @@ -473,7 +473,7 @@
    1.28  
    1.29  (*/--- final test ---------------------------------------------------------------------------\\*)
    1.30  val (res, asm) = (get_obj g_result pt (fst p));
    1.31 -if UnparseC.term2str res = "2 * a" andalso map UnparseC.term2str asm = []
    1.32 +if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
    1.33  andalso p = ([], Und) andalso msg = "end-of-calculation"
    1.34  andalso pr_ctree pr_short pt = ".    ----- pblobj -----\n1.   a + a\n"
    1.35  then 
    1.36 @@ -513,7 +513,7 @@
    1.37  ([1], Res), x + 1 + -1 * 2 = 0             ///Check_Postcond..ERROR*)
    1.38  
    1.39  (*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
    1.40 -"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: UnparseC.term_as_string) = ((**) "x = 1");
    1.41 +"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
    1.42      val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
    1.43      val pos = (*get_pos cI 1*) p
    1.44