1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -106,8 +106,8 @@
     1.4  
     1.5  ML \<open>
     1.6  val ansatz_rls = prep_rls'(
     1.7 -  Rule_Set.Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 
     1.8 -	  erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
     1.9 +  Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.10 +	  erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.11  	  rules = 
    1.12  	   [Rule.Thm ("ansatz_2nd_order",TermC.num_str @{thm ansatz_2nd_order}),
    1.13  	    Rule.Thm ("ansatz_3rd_order",TermC.num_str @{thm ansatz_3rd_order})
    1.14 @@ -115,8 +115,8 @@
    1.15  	 scr = Rule.EmptyScr});
    1.16  
    1.17  val equival_trans = prep_rls'(
    1.18 -  Rule_Set.Rls {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.19 -	  erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.20 +  Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.21 +	  erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.22  	  rules = 
    1.23  	   [Rule.Thm ("equival_trans_2nd_order",TermC.num_str @{thm equival_trans_2nd_order}),
    1.24  	    Rule.Thm ("equival_trans_3rd_order",TermC.num_str @{thm equival_trans_3rd_order})
    1.25 @@ -124,9 +124,9 @@
    1.26  	 scr = Rule.EmptyScr});
    1.27  
    1.28  val multiply_ansatz = prep_rls'(
    1.29 -  Rule_Set.Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.30 -	  erls = Rule_Set.Erls,
    1.31 -	  srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.32 +  Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.33 +	  erls = Rule_Set.Empty,
    1.34 +	  srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.35  	  rules = 
    1.36  	   [Rule.Thm ("multiply_2nd_order",TermC.num_str @{thm multiply_2nd_order})
    1.37  	   ], 
    1.38 @@ -163,7 +163,7 @@
    1.39  subsection \<open>Method\<close>
    1.40  text \<open>rule set for functions called in the Program\<close>
    1.41  ML \<open>
    1.42 -  val srls_partial_fraction = Rule_Set.Rls {id="srls_partial_fraction", 
    1.43 +  val srls_partial_fraction = Rule_Def.Repeat {id="srls_partial_fraction", 
    1.44      preconds = [],
    1.45      rew_ord = ("termlessI",termlessI),
    1.46      erls = Rule_Set.append_rls "erls_in_srls_partial_fraction" Rule_Set.e_rls
    1.47 @@ -171,7 +171,7 @@
    1.48         Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.49         (*2nd NTH_CONS pushes n+-1 into asms*)
    1.50         Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")], 
    1.51 -    srls = Rule_Set.Erls, calc = [], errpatts = [],
    1.52 +    srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.53      rules = [
    1.54         Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
    1.55         Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),