src/HOL/Library/conditional_parametricity.ML

--- a/src/HOL/Library/conditional_parametricity.ML	Wed Jul 26 11:59:55 2023 +0200
+++ b/src/HOL/Library/conditional_parametricity.ML	Wed Jul 26 12:58:47 2023 +0200
@@ -502,7 +502,7 @@
     val thm = prove_goal settings lthy (SOME eq) goal;
     val (res, lthy') = Local_Theory.note (b, [thm]) lthy;
     val _ = if #suppress_print_theorem settings then () else
-      Proof_Display.print_results true (Position.thread_data ()) lthy' (("theorem",""), [res]);
+      Proof_Display.print_theorem (Position.thread_data ()) lthy' res;
   in
     (the_single (snd res), lthy')
   end;