diff -r 2cbb98890190 -r 3e241a6938ce src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Mar 15 15:48:52 2018 +0100
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Fri Mar 23 10:14:39 2018 +0100
@@ -342,7 +342,7 @@
       (["integrate","function"],
         [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
           ("#Find"  ,["antiDerivative F_F"])],
-        Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], 
+        Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], 
         SOME "Integrate (f_f, v_v)", 
         [["diff","integration"]])),
     (*here "named" is used differently from Differentiation"*)
@@ -350,7 +350,7 @@
       (["named","integrate","function"],
         [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
           ("#Find"  ,["antiDerivativeName F_F"])],
-        Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], 
+        Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], 
         SOME "Integrate (f_f, v_v)", 
         [["diff","integration","named"]]))] *}