1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -69,10 +69,10 @@
     1.4  ML \<open>
     1.5      
     1.6  val LinPoly_simplify = prep_rls'(
     1.7 -  Rule_Set.Rls {id = "LinPoly_simplify", preconds = [], 
     1.8 +  Rule_Def.Repeat {id = "LinPoly_simplify", preconds = [], 
     1.9         rew_ord = ("termlessI",termlessI), 
    1.10         erls = LinEq_erls, 
    1.11 -       srls = Rule_Set.Erls, 
    1.12 +       srls = Rule_Set.Empty, 
    1.13         calc = [], errpatts = [],
    1.14         rules = [
    1.15  		Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
    1.16 @@ -93,10 +93,10 @@
    1.17  
    1.18  (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
    1.19  val LinEq_simplify = prep_rls'(
    1.20 -Rule_Set.Rls {id = "LinEq_simplify", preconds = [],
    1.21 +Rule_Def.Repeat {id = "LinEq_simplify", preconds = [],
    1.22       rew_ord = ("e_rew_ord", Rule.e_rew_ord),
    1.23       erls = LinEq_erls,
    1.24 -     srls = Rule_Set.Erls,
    1.25 +     srls = Rule_Set.Empty,
    1.26       calc = [], errpatts = [],
    1.27       rules = [
    1.28  	      Rule.Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}),