1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jun 21 16:18:27 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jun 21 20:06:12 2021 +0200
     1.3 @@ -76,8 +76,8 @@
     1.4  	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
     1.5    | eval_occur_exactly_in _ _ _ _ = NONE;
     1.6  \<close>
     1.7 -setup \<open>KEStore_Elems.add_calcs
     1.8 -  [("occur_exactly_in", (\<^const_name>\<open>occur_exactly_in\<close>, eval_occur_exactly_in "#eval_occur_exactly_in_"))]\<close>
     1.9 +calculation occur_exactly_in = \<open>eval_occur_exactly_in "#eval_occur_exactly_in_"\<close>
    1.10 +
    1.11  ML \<open>
    1.12  (** rewrite order 'ord_simplify_System' **)
    1.13