test/Tools/isac/ProgLang/listC.sml
changeset 60509 2e0b7ca391dc
parent 60500 59a3af532717
child 60543 9555ee96e046
     1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  TermC.atomty t;
     1.5  val thm = Thm.prop_of @{thm NTH_NIL};
     1.6  TermC.atomty thm;
     1.7 -val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false @{thm NTH_NIL} t;
     1.8 +val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t;
     1.9  if UnparseC.term t' = "a" then () 
    1.10  else error "NTH 1 [a,b,c,d,e] = a ..changed";
    1.11  
    1.12 @@ -66,7 +66,7 @@
    1.13  | _ => error "ListC.NTH changed";
    1.14  val thm = Thm.prop_of @{thm NTH_CONS};
    1.15  TermC.atomty thm;
    1.16 -val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false  @{thm NTH_CONS} t;
    1.17 +val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false  @{thm NTH_CONS} t;
    1.18  if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 
    1.19  else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
    1.20