test/Tools/isac/MathEngBasic/rewrite.sml
changeset 60543 9555ee96e046
parent 60519 70b30d910fd5
child 60565 f92963a33fe3
     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;