1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Jun 21 15:50:58 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Jun 21 16:18:27 2021 +0200
     1.3 @@ -25,21 +25,21 @@
     1.4  subsection \<open>setup for ML-functions\<close>
     1.5  text \<open>required by "eval_binop" below\<close>
     1.6  setup \<open>KEStore_Elems.add_calcs
     1.7 -  [ ("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "#occurs_in_")),
     1.8 -    ("some_occur_in", ("Prog_Expr.some_occur_in", Prog_Expr.eval_some_occur_in "#some_occur_in_")),
     1.9 -    ("is_atom", ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_")),
    1.10 -    ("is_even", ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_")),
    1.11 -    ("is_const", ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")),
    1.12 +  [ ("occurs_in", (\<^const_name>\<open>occurs_in\<close>, Prog_Expr.eval_occurs_in "#occurs_in_")),
    1.13 +    ("some_occur_in", (\<^const_name>\<open>some_occur_in\<close>, Prog_Expr.eval_some_occur_in "#some_occur_in_")),
    1.14 +    ("is_atom", (\<^const_name>\<open>is_atom\<close>, Prog_Expr.eval_is_atom "#is_atom_")),
    1.15 +    ("is_even", (\<^const_name>\<open>is_even\<close>, Prog_Expr.eval_is_even "#is_even_")),
    1.16 +    ("is_const", (\<^const_name>\<open>is_const\<close>, Prog_Expr.eval_const "#is_const_")),
    1.17      ("le", (\<^const_name>\<open>less\<close>, Prog_Expr.eval_equ "#less_")),
    1.18      ("leq", (\<^const_name>\<open>less_eq\<close>, Prog_Expr.eval_equ "#less_equal_")),
    1.19 -    ("ident", ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")),
    1.20 +    ("ident", (\<^const_name>\<open>ident\<close>, Prog_Expr.eval_ident "#ident_")),
    1.21      ("equal", (\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")),
    1.22      ("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
    1.23      ("MINUS", (\<^const_name>\<open>minus\<close>, (**)eval_binop "#sub_")),
    1.24      ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
    1.25      ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
    1.26      ("POWER",(\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_")),
    1.27 -    ("boollist2sum", ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum ""))]\<close>
    1.28 +    ("boollist2sum", (\<^const_name>\<open>boollist2sum\<close>, Prog_Expr.eval_boollist2sum ""))]\<close>
    1.29  
    1.30  subsection \<open>rewrite-order for rule-sets\<close>
    1.31  ML \<open>