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>, _) $ _) $