Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/proof_display.ML
changeset 80328 559909bd7715
parent 79540 afa75b58166a 
--- a/src/Pure/Isar/proof_display.ML	Mon Jun 10 14:04:52 2024 +0200
+++ b/src/Pure/Isar/proof_display.ML	Mon Jun 10 14:05:39 2024 +0200
@@ -369,10 +369,10 @@
     else
       print
         (case facts of
-          [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
-            Proof_Context.pretty_fact ctxt fact])
-        | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
-            Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]))
+          [fact] => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk,
+            Proof_Context.pretty_fact ctxt fact]
+        | _ => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk,
+            Pretty.block1 (Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])
   end;
 
 fun print_theorem pos ctxt fact =
isabelle