1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Jun 10 11:54:20 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Jun 10 12:23:57 2021 +0200
     1.3 @@ -330,7 +330,7 @@
     1.4  
     1.5  (** problems **)
     1.6  setup \<open>KEStore_Elems.add_pbts
     1.7 -  [(Problem.prep_input thy "pbl_fun_integ" [] Problem.id_empty
     1.8 +  [(Problem.prep_input @{theory} "pbl_fun_integ" [] Problem.id_empty
     1.9        (["integrate", "function"],
    1.10          [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.11            ("#Find"  ,["antiDerivative F_F"])],
    1.12 @@ -338,7 +338,7 @@
    1.13          SOME "Integrate (f_f, v_v)", 
    1.14          [["diff", "integration"]])),
    1.15      (*here "named" is used differently from Differentiation"*)
    1.16 -    (Problem.prep_input thy "pbl_fun_integ_nam" [] Problem.id_empty
    1.17 +    (Problem.prep_input @{theory} "pbl_fun_integ_nam" [] Problem.id_empty
    1.18        (["named", "integrate", "function"],
    1.19          [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.20            ("#Find"  ,["antiDerivativeName F_F"])],
    1.21 @@ -356,7 +356,7 @@
    1.22    in
    1.23      (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
    1.24  setup \<open>KEStore_Elems.add_mets
    1.25 -    [MethodC.prep_input thy "met_diffint" [] MethodC.id_empty
    1.26 +    [MethodC.prep_input @{theory} "met_diffint" [] MethodC.id_empty
    1.27  	    (["diff", "integration"],
    1.28  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find"  ,["antiDerivative F_F"])],
    1.29  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    1.30 @@ -374,7 +374,7 @@
    1.31      (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
    1.32      ) t_t)"
    1.33  setup \<open>KEStore_Elems.add_mets
    1.34 -    [MethodC.prep_input thy "met_diffint_named" [] MethodC.id_empty
    1.35 +    [MethodC.prep_input @{theory} "met_diffint_named" [] MethodC.id_empty
    1.36  	    (["diff", "integration", "named"],
    1.37  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.38  	        ("#Find"  ,["antiDerivativeName F_F"])],