src/Tools/isac/Knowledge/Base_Tools.thy
changeset 59851 4dd533681fef
parent 59850 f3cac3053e7b
child 59852 ea7e6679080e
     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>