# HG changeset patch
# User wenzelm
# Date 1631188049 -7200
# Node ID 5c110ac28dcff88affe562c645299e3a0c9515df
# Parent  612b7e0d67215424b740332b85176b08dca24aae
tuned whitespace;

diff -r 612b7e0d6721 -r 5c110ac28dcf src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML	Thu Sep 09 12:33:14 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML	Thu Sep 09 13:47:29 2021 +0200
@@ -95,9 +95,7 @@
     fun var_inst v y =
       let
         val ((x, i), T) = v;
-        val (U, args) =
-          if Vars.defined concl_vars v then (T, [])
-          else (Ts ---> T, ts);
+        val (U, args) = if Vars.defined concl_vars v then (T, []) else (Ts ---> T, ts);
         val u = Free (y, U);
         in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
     val (inst1, inst2) =