# HG changeset patch
# User wenzelm
# Date 1629372126 -7200
# Node ID b5eba47176482c71eac254f800eec84d6c572efe
# Parent  8e2355ddce1b1576eba32c05629e7f8345de0687# Parent  c6bce3633c530dca8a4681a2fe6aa8cd00ecd3c3
merged

diff -r 8e2355ddce1b -r b5eba4717648 src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Thu Aug 19 12:31:06 2021 +0200
+++ b/src/Pure/General/time.scala	Thu Aug 19 13:22:06 2021 +0200
@@ -14,8 +14,8 @@
 object Time
 {
   def seconds(s: Double): Time = new Time((s * 1000.0).round)
-  def minutes(s: Double): Time = new Time((s * 60000.0).round)
-  def ms(m: Long): Time = new Time(m)
+  def minutes(m: Double): Time = new Time((m * 60000.0).round)
+  def ms(ms: Long): Time = new Time(ms)
   def hms(h: Int, m: Int, s: Double): Time = seconds(s + 60 * m + 3600 * h)
 
   def now(): Time = ms(System.currentTimeMillis())
diff -r 8e2355ddce1b -r b5eba4717648 src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Thu Aug 19 12:31:06 2021 +0200
+++ b/src/Pure/General/timing.ML	Thu Aug 19 13:22:06 2021 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/General/timing.ML
     Author:     Makarius
 
-Basic support for time measurement.
+Support for time measurement.
 *)
 
 signature BASIC_TIMING =
diff -r 8e2355ddce1b -r b5eba4717648 src/Pure/System/bash.ML
--- a/src/Pure/System/bash.ML	Thu Aug 19 12:31:06 2021 +0200
+++ b/src/Pure/System/bash.ML	Thu Aug 19 13:22:06 2021 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/System/bash.ML
     Author:     Makarius
 
-Syntax for GNU bash.
+Support for GNU bash.
 *)
 
 signature BASH =
diff -r 8e2355ddce1b -r b5eba4717648 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Thu Aug 19 12:31:06 2021 +0200
+++ b/src/Pure/System/bash.scala	Thu Aug 19 13:22:06 2021 +0200
@@ -1,7 +1,8 @@
 /*  Title:      Pure/System/bash.scala
     Author:     Makarius
 
-GNU bash processes, with propagation of interrupts.
+Support for GNU bash: portable external processes with propagation of
+interrupts.
 */
 
 package isabelle
diff -r 8e2355ddce1b -r b5eba4717648 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Aug 19 12:31:06 2021 +0200
+++ b/src/Pure/proofterm.ML	Thu Aug 19 13:22:06 2021 +0200
@@ -266,8 +266,6 @@
   maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
   #> Lazy.consolidate #> map Lazy.force #> ignore;
 
-val consolidate_body = consolidate_bodies o single;
-
 fun make_thm_node theory_name name prop body export =
   let
     val consolidate =
@@ -1983,7 +1981,7 @@
     fun fulfill () =
       postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body));
   in
-    if null promises then Future.map (postproc #> tap consolidate_body) body
+    if null promises then Future.map postproc body
     else if Future.is_finished body andalso length promises = 1 then
       Future.map (fn _ => fulfill ()) (snd (hd promises))
     else