1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  subsection \<open>rule-sets\<close>
     1.5  ML \<open>
     1.6  \<close> ML \<open>
     1.7 -val Atools_erls = Rule_Set.append_rls "Atools_erls" Rule_Set.e_rls
     1.8 +val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty
     1.9    [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.10      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    1.11  		(*"(~ True) = False"*)
    1.12 @@ -89,7 +89,7 @@
    1.13  \<close>
    1.14  
    1.15  ML \<open>
    1.16 -val Atools_crls = Rule_Set.append_rls "Atools_crls" Rule_Set.e_rls
    1.17 +val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty
    1.18    [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.19      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    1.20  		Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
    1.21 @@ -117,7 +117,7 @@
    1.22  subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
    1.23  text \<open>requires "eval_binop" from above\<close>
    1.24  ML \<open>
    1.25 -val prog_expr = Rule_Set.append_rls "prog_expr" prog_expr
    1.26 +val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr
    1.27  	[ Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
    1.28  		Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), 
    1.29  		Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.30 @@ -130,10 +130,10 @@
    1.31  		Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
    1.32  		Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
    1.33  
    1.34 -val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge_rls "list_erls"
    1.35 +val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge "list_erls"
    1.36  	(Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
    1.37      erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 
    1.38 -    erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.39 +    erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.40      rules = [Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.41        Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
    1.42        (*    ~~~~~~ for nth_Cons_*)],