1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Mon May 11 18:06:24 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Mon May 11 20:49:27 2020 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  "----------- try fun applyTactics -----------------------";
     1.5  "----------- pbl binom polynom vereinfachen p.39 --------";
     1.6  "----------- pbl binom polynom vereinfachen: cube -------";
     1.7 -"----------- refine Vereinfache -------------------------";
     1.8 +"----------- Specify.refine Vereinfache -------------------------";
     1.9  "----------- *** prep_pbt: syntax error in '#Where' of [v";
    1.10  "--------------------------------------------------------";
    1.11  "--------------------------------------------------------";
    1.12 @@ -547,12 +547,12 @@
    1.13  if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "12 * a - 16 * q" 
    1.14  then () else error "pbl binom polynom vereinfachen: cube";
    1.15  
    1.16 -"----------- refine Vereinfache ----------------------------------";
    1.17 -"----------- refine Vereinfache ----------------------------------";
    1.18 -"----------- refine Vereinfache ----------------------------------";
    1.19 +"----------- Specify.refine Vereinfache ----------------------------------";
    1.20 +"----------- Specify.refine Vereinfache ----------------------------------";
    1.21 +"----------- Specify.refine Vereinfache ----------------------------------";
    1.22  val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"];
    1.23  (*default_print_depth 11;*)
    1.24 -val matches = refine fmz ["vereinfachen"];
    1.25 +val matches = Specify.refine fmz ["vereinfachen"];
    1.26  (*default_print_depth 3;*)
    1.27  
    1.28  "----- go into details, if it seems not to work -----";