1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -357,7 +357,7 @@
     1.4    in
     1.5      (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
     1.6  setup \<open>KEStore_Elems.add_mets
     1.7 -    [Method.prep_input thy "met_diffint" [] Method.id_empty
     1.8 +    [MethodC.prep_input thy "met_diffint" [] MethodC.id_empty
     1.9  	    (["diff", "integration"],
    1.10  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find"  ,["antiDerivative F_F"])],
    1.11  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    1.12 @@ -375,7 +375,7 @@
    1.13      (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
    1.14      ) t_t)"
    1.15  setup \<open>KEStore_Elems.add_mets
    1.16 -    [Method.prep_input thy "met_diffint_named" [] Method.id_empty
    1.17 +    [MethodC.prep_input thy "met_diffint_named" [] MethodC.id_empty
    1.18  	    (["diff", "integration", "named"],
    1.19  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.20  	        ("#Find"  ,["antiDerivativeName F_F"])],