--- 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;