1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -131,8 +131,8 @@
     1.4  ML \<open>
     1.5  \<close> ML \<open>
     1.6  val prog_expr =
     1.7 -  Rule_Def.Rls {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 
     1.8 -    erls = Rule_Def.Erls, srls = Rule_Def.Erls, calc = [], errpatts = [],
     1.9 +  Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 
    1.10 +    erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
    1.11      rules = [Rule_Def.Thm ("refl", TermC.num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
    1.12         Rule_Def.Thm ("o_apply", TermC.num_str @{thm o_apply}),
    1.13  
    1.14 @@ -176,7 +176,7 @@
    1.15         Rule_Def.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
    1.16         Rule_Def.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
    1.17         Rule_Def.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
    1.18 -    scr = Rule_Def.EmptyScr}: Rule_Set.rls;
    1.19 +    scr = Rule_Def.EmptyScr}: Rule_Set.T;
    1.20  \<close>
    1.21  setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>
    1.22