src/Pure/Isar/proof.ML

     val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
 
     fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
 
     val th =
-      (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
+      (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
         handle THM _ => err_lost ())
       |> Drule.flexflex_unique (SOME ctxt)
       |> Thm.check_shyps (Variable.sorts_of ctxt)
       |> Thm.check_hyps (Context.Proof ctxt);