1.1 --- a/test/Tools/isac/MathEngBasic/tactic.sml	Mon Apr 13 18:37:24 2020 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml	Tue Apr 14 12:39:26 2020 +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': theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * thm'' * term * result -> Tactic.T;
     1.8 +Rewrite': theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * ThmC.T * term * 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";