
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);
 \<close>




