1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -116,13 +116,13 @@
     1.4  "----------------------------------------------------------";
     1.5  
     1.6   val fod = make_deriv (@{theory "Isac_Knowledge"}) Atools_erls 
     1.7 -		       ((#rules o rep_rls) Test_simplify)
     1.8 +		       ((#rules o Rule_Set.rep) Test_simplify)
     1.9  		       (sqrt_right false (@{theory "Pure"})) NONE 
    1.10  		       (str2term "x + 1 + -1 * 2 = 0");
    1.11   (writeln o trtas2str) fod;
    1.12  
    1.13   val ifod = make_deriv (@{theory "Isac_Knowledge"}) Atools_erls 
    1.14 -		       ((#rules o rep_rls) Test_simplify)
    1.15 +		       ((#rules o Rule_Set.rep) Test_simplify)
    1.16  		       (sqrt_right false (@{theory "Pure"})) NONE 
    1.17  		       (str2term "-2 * 1 + (1 + x) = 0");
    1.18   (writeln o trtas2str) ifod;
    1.19 @@ -901,7 +901,7 @@
    1.20  val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");
    1.21  
    1.22  val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
    1.23 -  rew_sub thy 1 [] e_rew_ord e_rls false [] (HOLogic.Trueprop $ pat) res;
    1.24 +  rew_sub thy 1 [] e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.25  if rewritten then NONE else SOME "e_errpatID";
    1.26  
    1.27  val norm_res = case rewrite_set_ (Isac()) false rls res' of
    1.28 @@ -948,7 +948,7 @@
    1.29  val (res, inf) = (str2term "2 * x + d_d x (sin (x ^^^ 4))", str2term "2 * x + cos (4 * x ^^^ 3)");
    1.30  
    1.31  val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
    1.32 -  rew_sub thy 1 subst e_rew_ord e_rls false [] (HOLogic.Trueprop $ pat) res;
    1.33 +  rew_sub thy 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.34  if term2str res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then ()
    1.35  else error "build fun check_err_patt ?bdv changed 2";
    1.36  
    1.37 @@ -1111,7 +1111,7 @@
    1.38    val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
    1.39    (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
    1.40  val (form', _, _, rewritten) =
    1.41 -      rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (HOLogic.Trueprop $ pat) form;
    1.42 +      rew_sub (Isac()) 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
    1.43  
    1.44  if term2str form' = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
    1.45  else error "find_fillpatterns changed 3";
    1.46 @@ -1269,7 +1269,7 @@
    1.47  "--------- fun concat_deriv --------------------------------------";
    1.48  (*
    1.49   val ({rew_ord, erls, rules,...}, fo, ifo) = 
    1.50 -     (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
    1.51 +     (Rule_Set.rep Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
    1.52   (tracing o trtas2str) fod';
    1.53  > ["
    1.54  (x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","