diff -r 63cecf440235 -r 40eb8aa2b0d6 test/Tools/isac/ProgLang/listC.sml
--- a/test/Tools/isac/ProgLang/listC.sml	Mon Jun 21 22:08:01 2021 +0200
+++ b/test/Tools/isac/ProgLang/listC.sml	Sun Jul 18 18:15:27 2021 +0200
@@ -7,6 +7,7 @@
 "-----------------------------------------------------------------------------";
 "table of contents -----------------------------------------------------------";
 "-----------------------------------------------------------------------------";
+"----------- correct list_erls -----------------------------------------------------------------";
 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
 "--------------------- NTH ---------------------------------------------------";
 "--------------------- Length ------------------------------------------------";
@@ -14,6 +15,10 @@
 "-----------------------------------------------------------------------------";
 "-----------------------------------------------------------------------------";
 
+"----------- correct list_erls -----------------------------------------------------------------";
+"----------- correct list_erls -----------------------------------------------------------------";
+"----------- correct list_erls -----------------------------------------------------------------";
+
 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
 "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
@@ -50,22 +55,26 @@
 else error "NTH 1 [a,b,c,d,e] = a ..changed";
 
 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
-val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $
-  (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ 
-    (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
-TermC.atomty t;
+case TermC.str2term "NTH 3 [a,b,c,d,e]" of
+ Const ("ListC.NTH", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
+     (Const ("List.list.Cons", _) $ Free ("a", _) $
+       (Const ("List.list.Cons", _) $ Free ("b", _) $
+         (Const ("List.list.Cons", _) $ Free ("c", _) $
+           (Const ("List.list.Cons", _) $ Free ("d", _) $
+             (Const ("List.list.Cons", _) $ Free ("e", _) $ Const ("List.list.Nil", _)))))) => ()
+| _ => error "ListC.NTH changed";
 val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
 TermC.atomty thm;
 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
-if UnparseC.term t' = "NTH (3 + -1) [b, c, d, e]" then () 
+if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 
 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.str2term "NTH 3 [a,b,c,d,e]";
 TermC.atomty t;
-Rewrite.trace_on := false;
+Rewrite.trace_on := false; (*true false*)
 val SOME (t', _) = rewrite_set_ thy false prog_expr t;
-Rewrite.trace_on := false;
+Rewrite.trace_on := false; (*true false*)
 if UnparseC.term t' = "c" then () 
 else error "NTH 3 [a,b,c,d,e] = c ..changed";
 
@@ -95,6 +104,7 @@
 
 val t = TermC.str2term "Length [1, 1, 1]";
 val t = eval_prog_expr thy prog_expr t;
-case t of Free ("3", _) => () 
+case t of 
+  Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)) => () 
 | _ => error "Length [1, 1, 1] = 3  ..eval_prog_expr changed";