diff -r 83584916b6d7 -r 231b6d8231c6 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Mar 21 18:37:05 2025 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Mar 21 22:26:18 2025 +0100
@@ -617,8 +617,7 @@
         args thmss;
     val (res, lthy') = lthy |> Local_Theory.notes facts
     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 (res, lthy') end;
 
@@ -680,8 +679,7 @@
         map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
     val (res, lthy') = lthy |> Local_Theory.notes facts
     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 (res, lthy') end;