diff -r f3cac3053e7b -r 4dd533681fef src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Sat Apr 04 12:11:32 2020 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Apr 06 11:44:36 2020 +0200
@@ -69,10 +69,10 @@
 ML \<open>
     
 val LinPoly_simplify = prep_rls'(
-  Rule_Set.Rls {id = "LinPoly_simplify", preconds = [], 
+  Rule_Def.Repeat {id = "LinPoly_simplify", preconds = [], 
        rew_ord = ("termlessI",termlessI), 
        erls = LinEq_erls, 
-       srls = Rule_Set.Erls, 
+       srls = Rule_Set.Empty, 
        calc = [], errpatts = [],
        rules = [
 		Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
@@ -93,10 +93,10 @@
 
 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
 val LinEq_simplify = prep_rls'(
-Rule_Set.Rls {id = "LinEq_simplify", preconds = [],
+Rule_Def.Repeat {id = "LinEq_simplify", preconds = [],
      rew_ord = ("e_rew_ord", Rule.e_rew_ord),
      erls = LinEq_erls,
-     srls = Rule_Set.Erls,
+     srls = Rule_Set.Empty,
      calc = [], errpatts = [],
      rules = [
 	      Rule.Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}),