src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
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