diff -r 83584916b6d7 -r 231b6d8231c6 src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Fri Mar 21 18:37:05 2025 +0100
+++ b/src/HOL/Library/simps_case_conv.ML	Fri Mar 21 22:26:18 2025 +0100
@@ -117,8 +117,7 @@
     val thm = Attrib.eval_thms lthy thms_ref |> to_case lthy
     val (res, lthy') = Local_Theory.note (bind', [thm]) lthy 
     val _ =
-      Proof_Display.print_results
-        {interactive = int, pos = Position.thread_data (), proof_state = false}
+      Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}
         lthy' ((Thm.theoremK, ""), [res])
   in lthy' end
 
@@ -131,8 +130,7 @@
       else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm
     val (res, lthy') = Local_Theory.note (bind', simps) lthy
     val _ =
-      Proof_Display.print_results
-        {interactive = int, pos = Position.thread_data (), proof_state = false}
+      Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}
         lthy' ((Thm.theoremK, ""), [res])
   in lthy' end