1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Thu Sep 26 17:47:10 2019 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Tue Oct 01 10:47:25 2019 +0200
     1.3 @@ -572,14 +572,14 @@
     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 True @@\
     1.8 -\Try (Rewrite_Set Test_simplify False) @@\
     1.9 -\Try (Rewrite_Set rearrange_assoc False) @@\
    1.10 -\Try (Rewrite_Set Test_simplify False)) @@\
    1.11 -\Try (Rewrite_Set norm_equation False) @@\
    1.12 -\Try (Rewrite_Set Test_simplify False) @@\
    1.13 -\Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv False @@\
    1.14 -\Try (Rewrite_Set Test_simplify False))\
    1.15 +\Rewrite square_equation_left @@\
    1.16 +\Try (Rewrite_Set Test_simplify) @@\
    1.17 +\Try (Rewrite_Set rearrange_assoc) @@\
    1.18 +\Try (Rewrite_Set Test_simplify)) @@\
    1.19 +\Try (Rewrite_Set norm_equation) @@\
    1.20 +\Try (Rewrite_Set Test_simplify) @@\
    1.21 +\Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv @@\
    1.22 +\Try (Rewrite_Set Test_simplify))\
    1.23  \e_)";
    1.24  
    1.25  -------------------------*)