src/HOL/Tools/ATP/atp_proof_reconstruct.ML

     fun factify_step ((num, ss), role, t, rule, deps) =
       let
         val (ss', role', t') =
           (case resolve_conjectures ss of
             [j] =>
-            if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, nth hyp_ts j)
+            if j = length hyp_ts then ([], Conjecture, concl_t)
+            else ([], Hypothesis, close_form (nth hyp_ts j))
           | _ =>
             (case resolve_facts facts ss of
               [] => (ss, if role = Lemma then Lemma else Plain, t)
             | facts => (map fst facts, Axiom, t)))
       in