diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/MathEngBasic/tactic.sml
--- a/test/Tools/isac/MathEngBasic/tactic.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/MathEngBasic/tactic.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -18,7 +18,7 @@
 val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2});
 val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
 ;
-Rewrite': ThyC.id * Rule_Def.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T;
+Rewrite': ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T;
 val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res)
 ;
 if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED";