diff -r 05944144a692 -r 0763aec4c5b6 test/Tools/isac/Knowledge/polyminus.sml
--- a/test/Tools/isac/Knowledge/polyminus.sml	Mon May 11 18:06:24 2020 +0200
+++ b/test/Tools/isac/Knowledge/polyminus.sml	Mon May 11 20:49:27 2020 +0200
@@ -21,7 +21,7 @@
 "----------- try fun applyTactics -----------------------";
 "----------- pbl binom polynom vereinfachen p.39 --------";
 "----------- pbl binom polynom vereinfachen: cube -------";
-"----------- refine Vereinfache -------------------------";
+"----------- Specify.refine Vereinfache -------------------------";
 "----------- *** prep_pbt: syntax error in '#Where' of [v";
 "--------------------------------------------------------";
 "--------------------------------------------------------";
@@ -547,12 +547,12 @@
 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "12 * a - 16 * q" 
 then () else error "pbl binom polynom vereinfachen: cube";
 
-"----------- refine Vereinfache ----------------------------------";
-"----------- refine Vereinfache ----------------------------------";
-"----------- refine Vereinfache ----------------------------------";
+"----------- Specify.refine Vereinfache ----------------------------------";
+"----------- Specify.refine Vereinfache ----------------------------------";
+"----------- Specify.refine Vereinfache ----------------------------------";
 val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"];
 (*default_print_depth 11;*)
-val matches = refine fmz ["vereinfachen"];
+val matches = Specify.refine fmz ["vereinfachen"];
 (*default_print_depth 3;*)
 
 "----- go into details, if it seems not to work -----";