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