1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Thu Apr 29 09:55:06 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Thu Apr 29 11:36:11 2021 +0200
     1.3 @@ -216,7 +216,7 @@
     1.4                  Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
     1.5               in
     1.6                snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
     1.7 -             end) handle STOP_REW_SUB => false
     1.8 +             end) handle Pattern.MATCH => false
     1.9             fun scan_ _ [] = false
    1.10               | scan_ f (pp :: pps) =
    1.11                 if f pp then true else scan_ f pps;

     2.1 --- a/test/Tools/isac/Knowledge/poly.sml	Thu Apr 29 09:55:06 2021 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/poly.sml	Thu Apr 29 11:36:11 2021 +0200
     2.3 @@ -670,11 +670,11 @@
     2.4  "-------- norm_Poly NOT COMPLETE ------------------------";
     2.5  "-------- norm_Poly NOT COMPLETE ------------------------";
     2.6  "-------- norm_Poly NOT COMPLETE ------------------------";
     2.7 -val thy = @{theory Simplify};
     2.8 +val thy = @{theory AlgEin};
     2.9  
    2.10  val SOME (f',_) = rewrite_set_ thy false norm_Poly
    2.11  (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
    2.12 -if UnparseC.term f' = "L = 2 * 2 * (k + -2 * q) + senkrecht + oben"
    2.13 +if UnparseC.term f' = "L = senkrecht + oben + 2 * 2 * k + 2 * -4 * q"
    2.14  then ((*norm_Poly NOT COMPLETE -- TODO MG*))
    2.15  else error "norm_Poly changed behavior";
    2.16