1.1 --- a/test/Tools/isac/MathEngBasic/tactic.sml	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
     1.5  ;
     1.6  Rewrite': theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * thm'' * term * result -> Tactic.T;
     1.7 -val tac = Rewrite' ("Diff", "dummy_ord", e_rls, true, thm'', f, res)
     1.8 +val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res)
     1.9  ;
    1.10  if (Tactic.result tac |> term2str) = "a / b" then () else error "creates_assms CHANGED";
    1.11  if (Tactic.creates_assms tac |> terms2str) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED";