diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/ProgLang/listC.sml --- a/test/Tools/isac/ProgLang/listC.sml Wed Aug 03 18:17:27 2022 +0200 +++ b/test/Tools/isac/ProgLang/listC.sml Thu Aug 04 12:48:37 2022 +0200 @@ -51,7 +51,7 @@ TermC.atomty t; val thm = Thm.prop_of @{thm NTH_NIL}; TermC.atomty thm; -val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false @{thm NTH_NIL} t; +val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t; if UnparseC.term t' = "a" then () else error "NTH 1 [a,b,c,d,e] = a ..changed"; @@ -66,7 +66,7 @@ | _ => error "ListC.NTH changed"; val thm = Thm.prop_of @{thm NTH_CONS}; TermC.atomty thm; -val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false @{thm NTH_CONS} t; +val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_CONS} t; if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";