1.1 --- a/test/Tools/isac/ProgLang/listg.sml Tue Aug 31 16:00:13 2010 +0200
1.2 +++ b/test/Tools/isac/ProgLang/listg.sml Tue Aug 31 16:38:22 2010 +0200
1.3 @@ -14,7 +14,7 @@
1.4 atomty t;
1.5 val thm = (#prop o rep_thm o num_str) nth_Cons_;
1.6 atomty thm;
1.7 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Cons_) t;
1.8 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{nth_Cons_) t;
1.9 if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then ()
1.10 else raise error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
1.11
1.12 @@ -22,7 +22,7 @@
1.13 atomty t;
1.14 val thm = (#prop o rep_thm o num_str) nth_Nil_;
1.15 atomty thm;
1.16 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Nil_) t;
1.17 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{nth_Nil_) t;
1.18 term2str t';
1.19 "a";
1.20