1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Fri May 07 18:12:51 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Tue Jun 01 15:41:23 2021 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  "-----------------------------------------------------------------------------";
     1.5  "table of contents -----------------------------------------------------------";
     1.6  "-----------------------------------------------------------------------------";
     1.7 +"----------- correct list_erls -----------------------------------------------------------------";
     1.8  "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
     1.9  "--------------------- NTH ---------------------------------------------------";
    1.10  "--------------------- Length ------------------------------------------------";
    1.11 @@ -14,6 +15,10 @@
    1.12  "-----------------------------------------------------------------------------";
    1.13  "-----------------------------------------------------------------------------";
    1.14  
    1.15 +"----------- correct list_erls -----------------------------------------------------------------";
    1.16 +"----------- correct list_erls -----------------------------------------------------------------";
    1.17 +"----------- correct list_erls -----------------------------------------------------------------";
    1.18 +
    1.19  "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    1.20  "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    1.21  "----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    1.22 @@ -50,14 +55,18 @@
    1.23  else error "NTH 1 [a,b,c,d,e] = a ..changed";
    1.24  
    1.25  val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
    1.26 -val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const ("List.list.Cons", _) $ Free ("a", _) $
    1.27 -  (Const ("List.list.Cons", _) $ Free ("b", _) $ 
    1.28 -    (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
    1.29 -TermC.atomty t;
    1.30 +case TermC.str2term "NTH 3 [a,b,c,d,e]" of
    1.31 + Const ("ListC.NTH", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
    1.32 +     (Const ("List.list.Cons", _) $ Free ("a", _) $
    1.33 +       (Const ("List.list.Cons", _) $ Free ("b", _) $
    1.34 +         (Const ("List.list.Cons", _) $ Free ("c", _) $
    1.35 +           (Const ("List.list.Cons", _) $ Free ("d", _) $
    1.36 +             (Const ("List.list.Cons", _) $ Free ("e", _) $ Const ("List.list.Nil", _)))))) => ()
    1.37 +| _ => error "ListC.NTH changed";
    1.38  val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
    1.39  TermC.atomty thm;
    1.40  val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
    1.41 -if UnparseC.term t' = "NTH (3 + -1) [b, c, d, e]" then () 
    1.42 +if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 
    1.43  else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
    1.44  
    1.45  (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
    1.46 @@ -95,6 +104,7 @@
    1.47  
    1.48  val t = TermC.str2term "Length [1, 1, 1]";
    1.49  val t = eval_prog_expr thy prog_expr t;
    1.50 -case t of Free ("3", _) => () 
    1.51 +case t of 
    1.52 +  Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)) => () 
    1.53  | _ => error "Length [1, 1, 1] = 3  ..eval_prog_expr changed";
    1.54