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