author | wenzelm |
Thu, 09 Sep 2021 13:47:29 +0200 | |
changeset 74267 | 5c110ac28dcf |
parent 74266 | 612b7e0d6721 |
child 74268 | d01920a8b082 |
--- 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) =