test/Tools/isac/ProgLang/evaluate.sml
changeset 60509 2e0b7ca391dc
parent 60504 8cc1415b3530
child 60516 795d1352493a
     1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -56,22 +56,22 @@
     1.4  
     1.5  "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
     1.6  val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
     1.7 -val SOME (t', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
     1.8 +val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
     1.9  if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_  1 + 2 = 3  changed";
    1.10  
    1.11  "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
    1.12  val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
    1.13 -val SOME (t'', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
    1.14 +val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
    1.15  if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_  3 * 4 = 12  changed";
    1.16  
    1.17  "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
    1.18  val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
    1.19 -val SOME (t''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
    1.20 +val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
    1.21  if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_  12 / 3 = 4  changed";
    1.22  
    1.23  "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
    1.24  val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
    1.25 -val SOME (t'''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
    1.26 +val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
    1.27  if UnparseC.term t'''' = "16" then () else error "calculate_  12 / 3 = 4  changed";
    1.28  
    1.29  "----------- calculate from Prog --------------------------------- -----------------------------";