diff -r 35f7b2f61797 -r 8d89a214aedc src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jun 21 16:18:27 2021 +0200
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jun 21 20:06:12 2021 +0200
@@ -76,8 +76,8 @@
 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
   | eval_occur_exactly_in _ _ _ _ = NONE;
 \<close>
-setup \<open>KEStore_Elems.add_calcs
-  [("occur_exactly_in", (\<^const_name>\<open>occur_exactly_in\<close>, eval_occur_exactly_in "#eval_occur_exactly_in_"))]\<close>
+calculation occur_exactly_in = \<open>eval_occur_exactly_in "#eval_occur_exactly_in_"\<close>
+
 ML \<open>
 (** rewrite order 'ord_simplify_System' **)