1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Mar 15 15:48:52 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Fri Mar 23 10:14:39 2018 +0100
     1.3 @@ -451,7 +451,7 @@
     1.4          [("#Given", ["Term t_t"]),
     1.5            ("#Where", ["t_t is_polyexp"]),
     1.6            ("#Find", ["normalform n_n"])],
     1.7 -        Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)
     1.8 +        Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)
     1.9  			      Celem.Calc ("Poly.is'_polyexp", eval_is_polyexp "")], 
    1.10          SOME "Vereinfache t_t", 
    1.11          [["simplification","for_polynomials","with_parentheses_mult"]])),