diff -r e7910a62eaf2 -r 5037ca1b112b src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Apr 22 11:23:30 2020 +0200
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Apr 22 14:36:27 2020 +0200
@@ -331,7 +331,7 @@
 
 (** problems **)
 setup \<open>KEStore_Elems.add_pbts
-  [(Specify.prep_pbt thy "pbl_fun_integ" [] Spec.e_pblID
+  [(Specify.prep_pbt thy "pbl_fun_integ" [] Problem.id_empty
       (["integrate","function"],
         [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
           ("#Find"  ,["antiDerivative F_F"])],
@@ -339,7 +339,7 @@
         SOME "Integrate (f_f, v_v)", 
         [["diff","integration"]])),
     (*here "named" is used differently from Differentiation"*)
-    (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Spec.e_pblID
+    (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Problem.id_empty
       (["named","integrate","function"],
         [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
           ("#Find"  ,["antiDerivativeName F_F"])],
@@ -357,7 +357,7 @@
   in
     (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
 setup \<open>KEStore_Elems.add_mets
-    [Specify.prep_met thy "met_diffint" [] Spec.e_metID
+    [Specify.prep_met thy "met_diffint" [] Method.id_empty
 	    (["diff","integration"],
 	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find"  ,["antiDerivative F_F"])],
 	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
@@ -375,7 +375,7 @@
     (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
     ) t_t)"
 setup \<open>KEStore_Elems.add_mets
-    [Specify.prep_met thy "met_diffint_named" [] Spec.e_metID
+    [Specify.prep_met thy "met_diffint_named" [] Method.id_empty
 	    (["diff","integration","named"],
 	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
 	        ("#Find"  ,["antiDerivativeName F_F"])],