1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Wed Oct 02 15:14:51 2019 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Wed Oct 02 16:02:17 2019 +0200
     1.3 @@ -235,8 +235,8 @@
     1.4  "----------- met simplification for_polynomials with_minus -------";
     1.5  val str = 
     1.6  "Program SimplifyScript (t_t::real) =                \
     1.7 -\  (((Try (Rewrite_Set ordne_alphabetisch False)) @@     \
     1.8 -\    (Try (Rewrite_Set fasse_zusammen False)) @@     \
     1.9 +\  (((Try (Rewrite_Set ordne_alphabetisch False)) #>     \
    1.10 +\    (Try (Rewrite_Set fasse_zusammen False)) #>     \
    1.11  \    (Try (Rewrite_Set verschoenere False))) t_t)"
    1.12  val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
    1.13  atomty sc;
    1.14 @@ -341,8 +341,8 @@
    1.15  "Program ProbeScript (e_e::bool) (w_s::bool list) =\
    1.16  \ (let e_e = Take e_e;                             \
    1.17  \      e_e = Substitute w_s e_e                    \
    1.18 -\ in (Repeat((Try (Repeat (Calculate ''TIMES''))) @@  \
    1.19 -\            (Try (Repeat (Calculate ''PLUS''))) @@  \
    1.20 +\ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #>  \
    1.21 +\            (Try (Repeat (Calculate ''PLUS''))) #>  \
    1.22  \            (Try (Repeat (Calculate ''MINUS''))))) e_e)"
    1.23  val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
    1.24  atomty sc;