1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Dec 31 14:49:16 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Jan 10 18:17:48 2019 +0100
     1.3 @@ -363,7 +363,7 @@
     1.4  	        crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
     1.5  	      "Script 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'' False) (t_t::real))")]
     1.9  \<close>
    1.10  setup \<open>KEStore_Elems.add_mets
    1.11      [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
    1.12 @@ -374,8 +374,8 @@
    1.13            crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
    1.14          "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
    1.15            "  (let t_t = Take (F_F v_v = Integral f_f D v_v)                            " ^
    1.16 -          "   in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@  " ^
    1.17 -          "       (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_t)            ")]
    1.18 +          "   in ((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) @@  " ^
    1.19 +          "       (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False)) t_t)            ")]
    1.20  \<close>
    1.21  
    1.22  end
    1.23 \ No newline at end of file