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