1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Sat Apr 04 12:11:32 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Mon Apr 06 11:44:36 2020 +0200
1.3 @@ -131,14 +131,14 @@
1.4 Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
1.5
1.6 val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge_rls "list_erls"
1.7 - (Rule_Set.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
1.8 - erls = Rule_Set.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
1.9 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.10 + (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
1.11 + erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
1.12 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.13 rules = [Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.14 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
1.15 (* ~~~~~~ for nth_Cons_*)],
1.16 scr = Rule.EmptyScr},
1.17 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.18 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.19 rules = [], scr = Rule.EmptyScr})
1.20 prog_expr);
1.21 \<close>