# HG changeset patch
# User wenzelm
# Date 1160177477 -7200
# Node ID f625a65bfed5199a2fd6d62f2ad0a005e65e8a19
# Parent  0ddd2f297ae7ac2cf2775d347d84c6c135300c5b
added pretty_consts (from specification.ML);

diff -r 0ddd2f297ae7 -r f625a65bfed5 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Sat Oct 07 01:31:16 2006 +0200
+++ b/src/Pure/Isar/proof_display.ML	Sat Oct 07 01:31:17 2006 +0200
@@ -27,6 +27,7 @@
     ((string * string) * (string * thm list) list) -> unit
   val present_results: Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
+  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
 end
 
 structure ProofDisplay: PROOF_DISPLAY =
@@ -127,6 +128,26 @@
 
 end;
 
+
+(* consts *)
+
+local
+
+fun pretty_var ctxt (x, T) =
+  Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
+    Pretty.quote (ProofContext.pretty_typ ctxt T)];
+
+fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
+
+in
+
+fun pretty_consts ctxt pred cs =
+  (case filter pred (#1 (ProofContext.inferred_fixes ctxt)) of
+    [] => pretty_vars ctxt "constants" cs
+  | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
+
+end;
+
 end;
 
 structure BasicProofDisplay: BASIC_PROOF_DISPLAY = ProofDisplay;