1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Jun 21 16:18:27 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Jun 21 20:06:12 2021 +0200
     1.3 @@ -535,12 +535,12 @@
     1.4  subsection \<open>setup for rule-sets and ML-functions\<close>
     1.5  
     1.6  rule_set_knowledge prog_expr = prog_expr
     1.7 -setup \<open>KEStore_Elems.add_calcs
     1.8 -  [("matches", (\<^const_name>\<open>matches\<close>, Prog_Expr.eval_matches "#matches_")),
     1.9 -    ("matchsub", (\<^const_name>\<open>matchsub\<close>, Prog_Expr.eval_matchsub "#matchsub_")),
    1.10 -    ("Vars", (\<^const_name>\<open>Vars\<close>, Prog_Expr.eval_var "#Vars_")),
    1.11 -    ("lhs", (\<^const_name>\<open>lhs\<close>, Prog_Expr.eval_lhs "")),
    1.12 -    ("rhs", (\<^const_name>\<open>rhs\<close>, Prog_Expr.eval_rhs ""))]\<close>
    1.13 +
    1.14 +calculation matches = \<open>Prog_Expr.eval_matches "#matches_"\<close>
    1.15 +calculation matchsub = \<open>Prog_Expr.eval_matchsub "#matchsub_"\<close>
    1.16 +calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close>
    1.17 +calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close>
    1.18 +calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close>
    1.19  (*\\------------------------- from Tools .thy-------------------------------------------------//*)
    1.20  ML \<open>
    1.21  \<close> ML \<open>