1.1 --- a/test/Tools/isac/Knowledge/integrate.sml	Thu Sep 26 17:47:10 2019 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/integrate.sml	Tue Oct 01 10:47:25 2019 +0200
     1.3 @@ -377,14 +377,14 @@
     1.4  val str = 
     1.5  "Program IntegrationScript (f_f::real) (v_v::real) =               \
     1.6  \  (let t_t = Take (Integral f_f D v_v)                                 \
     1.7 -\   in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) (t_t::real))";
     1.8 +\   in (Rewrite_Set_Inst [(''bdv'',v_v)] integration) (t_t::real))";
     1.9  val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
    1.10  atomty sc;
    1.11  
    1.12  val str = 
    1.13  "Program NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
    1.14  \  (let t_t = Take (F_F v_v = Integral f_f D v_v)                         \
    1.15 -\   in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) t_t)";
    1.16 +\   in (Rewrite_Set_Inst [(''bdv'',v_v)] integration) t_t)";
    1.17  val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
    1.18  atomty sc;
    1.19  show_mets();