1.1 --- a/test/Tools/isac/Knowledge/atools.sml	Tue Jun 25 16:21:18 2019 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/atools.sml	Wed Jul 03 15:09:16 2019 +0200
     1.3 @@ -273,7 +273,7 @@
     1.4  if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
     1.5  else error "termorder.sml diff.behav ord_make_polynomial_in #14";
     1.6  
     1.7 -val SOME (t', _) = rewrite_set_inst_ thy false subst make_polynomial_in ppp;
     1.8 +val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
     1.9  if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
    1.10  else error "termorder.sml diff.behav ord_make_polynomial_in #15";
    1.11