1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Tue Sep 06 11:47:00 2022 +0200
1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Wed Sep 07 10:58:12 2022 +0200
1.3 @@ -489,7 +489,7 @@
1.4 val thy = @{theory RatEq};
1.5 val ctxt = Proof_Context.init_global thy;
1.6 val SOME t = TermC.parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
1.7 -val rls = assoc_rls "RatEq_eliminate"
1.8 +val rls = get_rls ctxt "RatEq_eliminate"
1.9
1.10 val SOME (t''''', asm''''') =
1.11 rewrite_set_ ctxt true rls t;