From b293fecf4c3c42390ef40289e7298da1d8893cef Mon Sep 17 00:00:00 2001
From: Yutaka Ng <7411634+yutakang@users.noreply.github.com>
Date: Mon, 4 Nov 2024 15:38:18 +0100
Subject: [PATCH] fix. This change should have included in the previous one.

---
 Abduction/All_Top_Down_Conjecturing.ML | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Abduction/All_Top_Down_Conjecturing.ML b/Abduction/All_Top_Down_Conjecturing.ML
index 4e52855b..b170d5fe 100644
--- a/Abduction/All_Top_Down_Conjecturing.ML
+++ b/Abduction/All_Top_Down_Conjecturing.ML
@@ -58,8 +58,8 @@ fun template_based_conjecture_for_simplification term2name (ctxt:Proof.context)
          (TBC.ctxt_n_const_to_identity     ctxt tm
         @ TBC.ctxt_n_const_to_idempotence  ctxt tm
         @ TBC.ctxt_n_const_to_zero_element ctxt tm
-        @ TBC.ctxt_n_consts_to_projection  ctxt tm
-        @ TBC.ctxt_n_consts_to_square      ctxt tm)
+        @ TBC.ctxt_n_consts_to_idempotence ctxt tm
+        @ TBC.ctxt_n_consts_to_involution  ctxt tm)
        |> map (apfst Template_Based_Conjecturing.property_as_string)
        |> map (fn (lemma_typ, term) => (SS.get_lemma_name term2name ctxt lemma_typ term, term));;
     val result = map (ctxt_n_const_to_all_conjecture_term ctxt) (relevant_unary_funcs @ relevant_binary_funcs)