1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Fri Apr 10 16:16:09 2020 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Fri Apr 10 18:32:36 2020 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_NIL};
     1.5  atomty thm;
     1.6  val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (num_str @{thm NTH_NIL}) t;
     1.7 -if UnparseC.term2str t' = "a" then () 
     1.8 +if UnparseC.term t' = "a" then () 
     1.9  else error "NTH 1 [a,b,c,d,e] = a ..changed";
    1.10  
    1.11  val t = str2term "NTH 3 [a,b,c,d,e]";
    1.12 @@ -57,7 +57,7 @@
    1.13  val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_CONS};
    1.14  atomty thm;
    1.15  val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (num_str @{thm NTH_CONS}) t;
    1.16 -if UnparseC.term2str t' = "NTH (3 + -1) [b, c, d, e]" then () 
    1.17 +if UnparseC.term t' = "NTH (3 + -1) [b, c, d, e]" then () 
    1.18  else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
    1.19  
    1.20  (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
    1.21 @@ -66,7 +66,7 @@
    1.22  trace_rewrite := false;
    1.23  val SOME (t', _) = rewrite_set_ thy false prog_expr t;
    1.24  trace_rewrite := false;
    1.25 -if UnparseC.term2str t' = "c" then () 
    1.26 +if UnparseC.term t' = "c" then () 
    1.27  else error "NTH 3 [a,b,c,d,e] = c ..changed";
    1.28  
    1.29  "--------------------- LENGTH ------------------------------------------------";
    1.30 @@ -77,20 +77,20 @@
    1.31  val thy = @{theory ListC};
    1.32  val t = str2term "LENGTH [1, 1, 1]";
    1.33  val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.34 -UnparseC.term2str t = "1 + LENGTH [1, 1]";
    1.35 +UnparseC.term t = "1 + LENGTH [1, 1]";
    1.36  val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.37 -UnparseC.term2str t = "1 + (1 + LENGTH [1])";
    1.38 +UnparseC.term t = "1 + (1 + LENGTH [1])";
    1.39  val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.40 -UnparseC.term2str t = "1 + (1 + (1 + LENGTH []))";
    1.41 +UnparseC.term t = "1 + (1 + (1 + LENGTH []))";
    1.42  val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.43  val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.44  val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.45 -if UnparseC.term2str t = "1 + (1 + (1 + 0))" then () 
    1.46 +if UnparseC.term t = "1 + (1 + (1 + 0))" then () 
    1.47  else error "LENGTH [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
    1.48  
    1.49  val t = str2term "LENGTH [1, 1, 1]";
    1.50  val SOME (t, asm) = rewrite_set_ thy false prog_expr t;
    1.51 -if UnparseC.term2str t = "3" then ()
    1.52 +if UnparseC.term t = "3" then ()
    1.53  else error "LENGTH [1, 1, 1] = 3  ..prog_expr changed";
    1.54  
    1.55  val t = str2term "LENGTH [1, 1, 1]";