1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -965,7 +965,7 @@
     1.4  term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
     1.5  
     1.6  val thm = num_str @{thm square_explicit1};
     1.7 -val SOME (t,asm) = rewrite_ thy dummy_ord Erls true thm t;
     1.8 +val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
     1.9  term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
    1.10  
    1.11  val thm = num_str @{thm root_plus_minus};
    1.12 @@ -975,17 +975,17 @@
    1.13  
    1.14  (*the thm bdv_explicit2* here required to be constrained to ::real*)
    1.15  val thm = num_str @{thm bdv_explicit2};
    1.16 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
    1.17 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
    1.18  term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
    1.19                "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
    1.20  
    1.21  val thm = num_str @{thm bdv_explicit3};
    1.22 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
    1.23 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
    1.24  term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
    1.25                     "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
    1.26  
    1.27  val thm = num_str @{thm bdv_explicit2};
    1.28 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
    1.29 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
    1.30  term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
    1.31                  "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
    1.32