1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Sun Feb 09 16:21:26 2020 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Sun Feb 09 16:55:41 2020 +0100
     1.3 @@ -130,8 +130,8 @@
     1.4  subsection \<open>rule set for evaluating Porg_Expr, will be extended in several thys\<close>
     1.5  ML \<open>
     1.6  \<close> ML \<open>
     1.7 -val list_rls = 
     1.8 -  Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 
     1.9 +val prog_expr = 
    1.10 +  Rule.Rls {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 
    1.11      erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
    1.12      rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
    1.13         Rule.Thm ("o_apply", TermC.num_str @{thm o_apply}),
    1.14 @@ -178,6 +178,6 @@
    1.15         Rule.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
    1.16      scr = Rule.EmptyScr}: Rule.rls;
    1.17  \<close>
    1.18 -setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>
    1.19 +setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>
    1.20  
    1.21  end