1.1 --- a/test/Tools/isac/ProgLang/listC.sml Mon Apr 13 13:27:55 2020 +0200
1.2 +++ b/test/Tools/isac/ProgLang/listC.sml Mon Apr 13 15:31:23 2020 +0200
1.3 @@ -43,9 +43,9 @@
1.4
1.5 val t = str2term "NTH 1 [a,b,c,d,e]";
1.6 atomty t;
1.7 -val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_NIL};
1.8 +val thm = (#prop o Thm.rep_thm o ThmC.numerals_to_Free) @{thm NTH_NIL};
1.9 atomty thm;
1.10 -val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (num_str @{thm NTH_NIL}) t;
1.11 +val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_NIL}) t;
1.12 if UnparseC.term t' = "a" then ()
1.13 else error "NTH 1 [a,b,c,d,e] = a ..changed";
1.14
1.15 @@ -54,9 +54,9 @@
1.16 (Const ("List.list.Cons", _) $ Free ("b", _) $
1.17 (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
1.18 atomty t;
1.19 -val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_CONS};
1.20 +val thm = (#prop o Thm.rep_thm o ThmC.numerals_to_Free) @{thm NTH_CONS};
1.21 atomty thm;
1.22 -val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (num_str @{thm NTH_CONS}) t;
1.23 +val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
1.24 if UnparseC.term t' = "NTH (3 + -1) [b, c, d, e]" then ()
1.25 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
1.26