diff -r 873f40b097bb -r c4b24621077e test/Tools/isac/ProgLang/listC.sml
--- a/test/Tools/isac/ProgLang/listC.sml	Sun Jan 29 14:31:56 2023 +0100
+++ b/test/Tools/isac/ProgLang/listC.sml	Mon Jan 30 09:47:18 2023 +0100
@@ -47,7 +47,7 @@
 val ctxt = Proof_Context.init_global @{theory}
 val prog_expr = get_rls @{context} "prog_expr"
 
-val t = TermC.parse_test @{context} "NTH 1 [a,b,c,d,e]";
+val t = ParseC.parse_test @{context} "NTH 1 [a,b,c,d,e]";
 TermC.atom_trace_detail @{context} t;
 val thm = Thm.prop_of @{thm NTH_NIL};
 TermC.atom_trace_detail @{context} thm;
@@ -55,8 +55,8 @@
 if UnparseC.term t' = "a" then () 
 else error "NTH 1 [a,b,c,d,e] = a ..changed";
 
-val t = TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]";
-case TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]" of
+val t = ParseC.parse_test @{context} "NTH 3 [a,b,c,d,e]";
+case ParseC.parse_test @{context} "NTH 3 [a,b,c,d,e]" of
  Const (\<^const_name>\<open>NTH\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
      (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $
        (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $
@@ -71,7 +71,7 @@
 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
 
 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
-val t = TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]";
+val t = ParseC.parse_test @{context} "NTH 3 [a,b,c,d,e]";
 TermC.atom_trace_detail @{context} t;
 
 val SOME (t', _) = rewrite_set_ ctxt false prog_expr t;
@@ -84,7 +84,7 @@
 val prog_expr = get_rls @{context} "prog_expr"
 
 val thy = @{theory ListC};
-val t = TermC.parse_test @{context} "Length [1, 1, 1]";
+val t = ParseC.parse_test @{context} "Length [1, 1, 1]";
 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
 UnparseC.term t = "1 + Length [1, 1]";
 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
@@ -97,12 +97,12 @@
 if UnparseC.term t = "1 + (1 + (1 + 0))" then () 
 else error "Length [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
 
-val t = TermC.parse_test @{context} "Length [1, 1, 1]";
+val t = ParseC.parse_test @{context} "Length [1, 1, 1]";
 val SOME (t, asm) = rewrite_set_ ctxt false prog_expr t;
 if UnparseC.term t = "3" then ()
 else error "Length [1, 1, 1] = 3  ..prog_expr changed";
 
-val t = TermC.parse_test @{context} "Length [1, 1, 1]";
+val t = ParseC.parse_test @{context} "Length [1, 1, 1]";
 val t = eval_prog_expr ctxt prog_expr t;
 case t of 
   Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => ()