1.1 --- a/test/Tools/isac/MathEngBasic/tactic.sml	Thu Apr 09 12:03:14 2020 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml	Thu Apr 09 17:13:17 2020 +0200
     1.3 @@ -21,5 +21,5 @@
     1.4  Rewrite': theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * thm'' * term * result -> Tactic.T;
     1.5  val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res)
     1.6  ;
     1.7 -if (Tactic.result tac |> term2str) = "a / b" then () else error "creates_assms CHANGED";
     1.8 -if (Tactic.creates_assms tac |> terms2str) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED";
     1.9 +if (Tactic.result tac |> UnparseC.term2str) = "a / b" then () else error "creates_assms CHANGED";
    1.10 +if (Tactic.creates_assms tac |> UnparseC.terms2str) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED";