1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -78,13 +78,13 @@
     1.4  val od = ord_make_polynomial true (@{theory "Poly"});
     1.5  val t = str2term "((a + d) + c) + b";
     1.6  "((a + d) + c) + b"; 
     1.7 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t; term2str t;
     1.8 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; term2str t;
     1.9  "b + ((a + d) + c)";
    1.10 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t; term2str t;
    1.11 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; term2str t;
    1.12  "b + (c + (a + d))";
    1.13 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    1.14 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;term2str t;
    1.15  "b + (a + (c + d))";
    1.16 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    1.17 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;term2str t;
    1.18  "a + (b + (c + d))";
    1.19  if term2str t = "a + (b + (c + d))" then ()
    1.20  else error "polyminus.sml 2 watch order_add_mult";
    1.21 @@ -92,11 +92,11 @@
    1.22  "----- if parentheses are right, left_commute is (almost) sufficient...";
    1.23  val t = str2term "a + (d + (c + b))";
    1.24  "a + (d + (c + b))";
    1.25 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    1.26 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;term2str t;
    1.27  "a + (c + (d + b))";
    1.28 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t;term2str t;
    1.29 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t;term2str t;
    1.30  "a + (c + (b + d))";
    1.31 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    1.32 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;term2str t;
    1.33  "a + (b + (c + d))";
    1.34  
    1.35  "----- but we do not want the parentheses at right; thus: cond.rew.";
    1.36 @@ -109,8 +109,8 @@
    1.37  "----- here we see rew_sub going into subterm with ord.rew....";
    1.38  val od = ord_make_polynomial false (@{theory "Poly"});
    1.39  val t = str2term "b + a + c + d";
    1.40 -val SOME (t,_) = rewrite_ thy od e_rls false @{thm add.commute} t; term2str t;
    1.41 -val SOME (t,_) = rewrite_ thy od e_rls false @{thm add.commute} t; term2str t;
    1.42 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; term2str t;
    1.43 +val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; term2str t;
    1.44  (*@@@ rew_sub gosub: t = d + (b + a + c)
    1.45    @@@ rew_sub begin: t = b + a + c*)
    1.46  
    1.47 @@ -566,7 +566,7 @@
    1.48    | _ => error "polyminus.sml matchsub (?a * (?b - ?c)...A";
    1.49  
    1.50  "--- does the respective prls rewrite ?";
    1.51 -val prls = append_rls "prls_pbl_vereinf_poly" e_rls 
    1.52 +val prls = Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty 
    1.53  	     [Num_Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
    1.54  	      Num_Calc ("Prog_Expr.matchsub", eval_matchsub ""),
    1.55  	      Thm ("or_true",@{thm or_true}),