test/Tools/isac/ProgLang/listg.sml
branchisac-update-Isa09-2
changeset 37967 bd4f7a35e892
parent 37960 ec20007095f2
child 37970 6df5d02e46ba
     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