diff -r f3cac3053e7b -r 4dd533681fef src/Tools/isac/Knowledge/Base_Tools.thy --- a/src/Tools/isac/Knowledge/Base_Tools.thy Sat Apr 04 12:11:32 2020 +0200 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Mon Apr 06 11:44:36 2020 +0200 @@ -131,14 +131,14 @@ Rule.Thm ("if_False",TermC.num_str @{thm if_False})]; val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge_rls "list_erls" - (Rule_Set.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI), - erls = Rule_Set.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [], + (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI), + erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [], rules = [Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_") (* ~~~~~~ for nth_Cons_*)], scr = Rule.EmptyScr}, - srls = Rule_Set.Erls, calc = [], errpatts = [], + srls = Rule_Set.Empty, calc = [], errpatts = [], rules = [], scr = Rule.EmptyScr}) prog_expr); \