diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/ProgLang/evaluate.sml --- a/test/Tools/isac/ProgLang/evaluate.sml Wed Aug 03 18:17:27 2022 +0200 +++ b/test/Tools/isac/ProgLang/evaluate.sml Thu Aug 04 12:48:37 2022 +0200 @@ -56,22 +56,22 @@ "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t); val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t; -val SOME (t', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t; +val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; if UnparseC.term t' = "(3 * 4 / 3) \ 2" then () else error "calculate_ 1 + 2 = 3 changed"; "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t'); val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t'; -val SOME (t'', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t; +val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; if UnparseC.term t'' = "(12 / 3) \ 2" then () else error "calculate_ 3 * 4 = 12 changed"; "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t''); val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t; -val SOME (t''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t; +val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; if UnparseC.term t''' = "4 \ 2" then () else error "calculate_ 12 / 3 = 4 changed"; "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t'''); val SOME ("#: 4 \ 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t; -val SOME (t'''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t; +val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed"; "----------- calculate from Prog --------------------------------- -----------------------------";