1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Wed Oct 02 15:14:51 2019 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Wed Oct 02 16:02:17 2019 +0200
     1.3 @@ -572,13 +572,13 @@
     1.4  
     1.5  val ttt = (Thm.term_of o the o (parse Test.thy))
     1.6  "Let (((While contains_root e_e Do\
     1.7 -\Rewrite square_equation_left @@\
     1.8 -\Try (Rewrite_Set Test_simplify) @@\
     1.9 -\Try (Rewrite_Set rearrange_assoc) @@\
    1.10 -\Try (Rewrite_Set Test_simplify)) @@\
    1.11 -\Try (Rewrite_Set norm_equation) @@\
    1.12 -\Try (Rewrite_Set Test_simplify) @@\
    1.13 -\Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv @@\
    1.14 +\Rewrite square_equation_left #>\
    1.15 +\Try (Rewrite_Set Test_simplify) #>\
    1.16 +\Try (Rewrite_Set rearrange_assoc) #>\
    1.17 +\Try (Rewrite_Set Test_simplify)) #>\
    1.18 +\Try (Rewrite_Set norm_equation) #>\
    1.19 +\Try (Rewrite_Set Test_simplify) #>\
    1.20 +\Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv #>\
    1.21  \Try (Rewrite_Set Test_simplify))\
    1.22  \e_)";
    1.23