changeset 82643 | f1c14af17591 |
parent 74525 | c960bfcb91db |
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Wed May 21 10:30:33 2025 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Wed May 21 10:30:34 2025 +0200 @@ -652,7 +652,7 @@ asm_full_simp_tac (Simplifier.add_simp @{lemma "(A & B) & C == A & B & C" by auto} (*FIXME duplicates @{thm simp_meta(3)}*) - (Raw_Simplifier.empty_simpset ctxt)) + (Simplifier.empty_simpset ctxt)) #> CHANGED #> REPEAT_DETERM