test/Tools/isac/MathEngBasic/rewrite.sml
changeset 60504 8cc1415b3530
parent 60500 59a3af532717
child 60509 2e0b7ca391dc
     1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Sun Jul 31 13:45:20 2022 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Sun Jul 31 16:35:33 2022 +0200
     1.3 @@ -374,7 +374,7 @@
     1.4  if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
     1.5  val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
     1.6  
     1.7 -(*+*)case eval_is_multUnordered "testid" "" tm thy of
     1.8 +(*+*)case eval_is_multUnordered "testid" "" tm ctxt of
     1.9  (*+*)  SOME
    1.10  (*+*)    ("testidx \<up> 2 * x_",
    1.11  (*+*)     Const (\<^const_name>\<open>Trueprop\<close>, _) $
    1.12 @@ -387,9 +387,9 @@
    1.13  (*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
    1.14  
    1.15  
    1.16 -     eval_is_multUnordered "testid" "" tm thy;
    1.17 +     eval_is_multUnordered "testid" "" tm ctxt;
    1.18  
    1.19 -case eval_is_multUnordered "testid" "" tm thy of
    1.20 +case eval_is_multUnordered "testid" "" tm ctxt of
    1.21      SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ 
    1.22                     (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
    1.23                            (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $