1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Wed Dec 02 12:32:30 2020 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Mon Dec 07 17:39:21 2020 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  "-----------------------------------------------------------------------------";
     1.5  "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
     1.6  "--------------------- NTH ---------------------------------------------------";
     1.7 -"--------------------- LENGTH ------------------------------------------------";
     1.8 +"--------------------- Length ------------------------------------------------";
     1.9  "--------------------- tl ----------------------------------------------------";
    1.10  "-----------------------------------------------------------------------------";
    1.11  "-----------------------------------------------------------------------------";
    1.12 @@ -69,32 +69,32 @@
    1.13  if UnparseC.term t' = "c" then () 
    1.14  else error "NTH 3 [a,b,c,d,e] = c ..changed";
    1.15  
    1.16 -"--------------------- LENGTH ------------------------------------------------";
    1.17 -"--------------------- LENGTH ------------------------------------------------";
    1.18 -"--------------------- LENGTH ------------------------------------------------";
    1.19 +"--------------------- Length ------------------------------------------------";
    1.20 +"--------------------- Length ------------------------------------------------";
    1.21 +"--------------------- Length ------------------------------------------------";
    1.22  val prog_expr = assoc_rls "prog_expr"
    1.23  
    1.24  val thy = @{theory ListC};
    1.25 -val t = str2term "LENGTH [1, 1, 1]";
    1.26 +val t = str2term "Length [1, 1, 1]";
    1.27  val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.28 -UnparseC.term t = "1 + LENGTH [1, 1]";
    1.29 +UnparseC.term t = "1 + Length [1, 1]";
    1.30  val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.31 -UnparseC.term t = "1 + (1 + LENGTH [1])";
    1.32 +UnparseC.term t = "1 + (1 + Length [1])";
    1.33  val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.34 -UnparseC.term t = "1 + (1 + (1 + LENGTH []))";
    1.35 +UnparseC.term t = "1 + (1 + (1 + Length []))";
    1.36  val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.37  val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.38  val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.39  if UnparseC.term t = "1 + (1 + (1 + 0))" then () 
    1.40 -else error "LENGTH [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
    1.41 +else error "Length [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
    1.42  
    1.43 -val t = str2term "LENGTH [1, 1, 1]";
    1.44 +val t = str2term "Length [1, 1, 1]";
    1.45  val SOME (t, asm) = rewrite_set_ thy false prog_expr t;
    1.46  if UnparseC.term t = "3" then ()
    1.47 -else error "LENGTH [1, 1, 1] = 3  ..prog_expr changed";
    1.48 +else error "Length [1, 1, 1] = 3  ..prog_expr changed";
    1.49  
    1.50 -val t = str2term "LENGTH [1, 1, 1]";
    1.51 +val t = str2term "Length [1, 1, 1]";
    1.52  val t = eval_prog_expr thy prog_expr t;
    1.53  case t of Free ("3", _) => () 
    1.54 -| _ => error "LENGTH [1, 1, 1] = 3  ..eval_prog_expr changed";
    1.55 +| _ => error "Length [1, 1, 1] = 3  ..eval_prog_expr changed";
    1.56