# HG changeset patch
# User wenzelm
# Date 1583765424 -3600
# Node ID 50ac132a49bbbc8b3f15f3b00869a66fc90522b0
# Parent  046cf49162a3f8de3955ba8f96787841baccbfb0
tuned whitespace;

diff -r 046cf49162a3 -r 50ac132a49bb src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Mar 09 15:38:52 2020 +0100
+++ b/src/Pure/proofterm.ML	Mon Mar 09 15:50:24 2020 +0100
@@ -1637,18 +1637,19 @@
       | SOME T' => chaseT env T')
   | chaseT _ T = T;
 
-fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs
-      (t as Const (s, T)) = if T = dummyT then
+fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs (t as Const (s, T)) =
+      if T = dummyT then
         (case Sign.const_type thy s of
           NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
         | SOME T =>
-            let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
-            in (Const (s, T'), T', vTs,
-              Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv})
+            let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T) in
+              (Const (s, T'), T', vTs,
+                Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv})
             end)
       else (t, T, vTs, env)
   | infer_type _ env _ vTs (t as Free (s, T)) =
-      if T = dummyT then (case Symtab.lookup vTs s of
+      if T = dummyT then
+        (case Symtab.lookup vTs s of
           NONE =>
             let val (T, env') = mk_tvar [] env
             in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end
@@ -1664,7 +1665,8 @@
       let
         val (t', T, vTs1, env1) = infer_type thy env Ts vTs t;
         val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u;
-      in (case chaseT env2 T of
+      in
+        (case chaseT env2 T of
           Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U')
         | _ =>
           let val (V, env3) = mk_tvar [] env2