diff -r 4dd533681fef -r ea7e6679080e src/Tools/isac/Knowledge/DiophantEq.thy
--- a/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Apr 06 11:44:36 2020 +0200
+++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Wed Apr 08 12:32:51 2020 +0200
@@ -21,7 +21,7 @@
           (*                                      TODO: drop ^^^^^*)
           ("#Where" ,[]),
           ("#Find"  ,["boolTestFind s_s"])],
-        Rule_Set.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close>
+        Rule_Set.empty, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close>
 
 text \<open>method solving the usecase\<close>
 
@@ -39,7 +39,7 @@
           (*                                      TODO: drop ^^^^^*)
           ("#Where" ,[]),
           ("#Find"  ,["boolTestFind s_s"])],
-        {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.e_rls, prls = Rule_Set.e_rls, calc = [],
+        {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
           crls = tval_rls, errpats = [], nrls = Test_simplify},
         @{thm diophant_equation.simps})]
 \<close>