1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Wed May 13 12:14:49 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Wed May 13 16:10:22 2020 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  "----------- pbl binom polynom vereinfachen p.39 --------";
     1.5  "----------- pbl binom polynom vereinfachen: cube -------";
     1.6  "----------- Refine.refine Vereinfache -------------------------";
     1.7 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
     1.8 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11  "--------------------------------------------------------";
    1.12 @@ -593,9 +593,9 @@
    1.13  if UnparseC.term t' = "False" then ()
    1.14  else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
    1.15  
    1.16 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
    1.17 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
    1.18 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
    1.19 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
    1.20 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
    1.21 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
    1.22  (*see test/../termC.sml for details*)
    1.23  val t = parse_patt thy "t_t is_polyexp";
    1.24  val t = parse_patt thy ("Not (matchsub (?a + (?b + ?c)) t_t | " ^