# HG changeset patch
# User wenzelm
# Date 1690369127 -7200
# Node ID 4dffc47b7e914a7038c5826156e6b6d13c08ee52
# Parent  12af46f2cd9405295ec65f179d1d373061d36fcb
tuned signature: more operations;

diff -r 12af46f2cd94 -r 4dffc47b7e91 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;
diff -r 12af46f2cd94 -r 4dffc47b7e91 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Jul 26 11:59:55 2023 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Jul 26 12:58:47 2023 +0200
@@ -26,6 +26,7 @@
   val show_results: bool Config.T
   val print_results: bool -> Position.T -> Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
+  val print_theorem: Position.T -> Proof.context -> string * thm list -> unit
   val print_consts: bool -> Position.T -> Proof.context ->
     (string * typ -> bool) -> (string * typ) list -> unit
   val markup_extern_label: Position.T -> (Markup.T * xstring) option
@@ -362,6 +363,9 @@
       | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
           Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
 
+fun print_theorem pos ctxt fact =
+  print_results true pos ctxt ((Thm.theoremK, ""), [fact]);
+
 end;