1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Sun Feb 09 16:21:26 2020 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Sun Feb 09 16:55:41 2020 +0100
     1.3 @@ -39,13 +39,13 @@
     1.4  "--------------------- NTH ---------------------------------------------------";
     1.5  "--------------------- NTH ---------------------------------------------------";
     1.6  "--------------------- NTH ---------------------------------------------------";
     1.7 -val list_rls = assoc_rls "list_rls"
     1.8 +val prog_expr = assoc_rls "prog_expr"
     1.9  
    1.10  val t = str2term "NTH 1 [a,b,c,d,e]";
    1.11  atomty t;
    1.12  val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_NIL};
    1.13  atomty thm;
    1.14 -val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_NIL}) t;
    1.15 +val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (num_str @{thm NTH_NIL}) t;
    1.16  if term2str t' = "a" then () 
    1.17  else error "NTH 1 [a,b,c,d,e] = a ..changed";
    1.18  
    1.19 @@ -56,7 +56,7 @@
    1.20  atomty t;
    1.21  val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_CONS};
    1.22  atomty thm;
    1.23 -val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_CONS}) t;
    1.24 +val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (num_str @{thm NTH_CONS}) t;
    1.25  if term2str t' = "NTH (3 + -1) [b, c, d, e]" then () 
    1.26  else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
    1.27  
    1.28 @@ -64,7 +64,7 @@
    1.29  val t = str2term "NTH 3 [a,b,c,d,e]";
    1.30  atomty t;
    1.31  trace_rewrite := false;
    1.32 -val SOME (t', _) = rewrite_set_ thy false list_rls t;
    1.33 +val SOME (t', _) = rewrite_set_ thy false prog_expr t;
    1.34  trace_rewrite := false;
    1.35  if term2str t' = "c" then () 
    1.36  else error "NTH 3 [a,b,c,d,e] = c ..changed";
    1.37 @@ -72,7 +72,7 @@
    1.38  "--------------------- LENGTH ------------------------------------------------";
    1.39  "--------------------- LENGTH ------------------------------------------------";
    1.40  "--------------------- LENGTH ------------------------------------------------";
    1.41 -val list_rls = assoc_rls "list_rls"
    1.42 +val prog_expr = assoc_rls "prog_expr"
    1.43  
    1.44  val thy = @{theory ListC};
    1.45  val t = str2term "LENGTH [1, 1, 1]";
    1.46 @@ -89,12 +89,12 @@
    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 list_rls t;
    1.51 +val SOME (t, asm) = rewrite_set_ thy false prog_expr t;
    1.52  if term2str t = "3" then ()
    1.53 -else error "LENGTH [1, 1, 1] = 3  ..list_rls changed";
    1.54 +else error "LENGTH [1, 1, 1] = 3  ..prog_expr changed";
    1.55  
    1.56  val t = str2term "LENGTH [1, 1, 1]";
    1.57 -val t = eval_prog_expr thy list_rls t;
    1.58 +val t = eval_prog_expr thy prog_expr t;
    1.59  case t of Free ("3", _) => () 
    1.60  | _ => error "LENGTH [1, 1, 1] = 3  ..eval_prog_expr changed";
    1.61