src/Pure/Isar/proof.ML

           |> fold_burrow (Assumption.add_assms Assumption.assume_export)
               ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
           |> (fn (premss, ctxt') => ctxt'
                 |> not (null assumes_propss) ?
                   (snd o Proof_Context.note_thmss ""
-                    [((Binding.name Auto_Bind.premsN, []),
+                    [((Binding.name Auto_Bind.thatN, []),
                       [(Assumption.local_prems_of ctxt' ctxt, [])])])
                 |> (snd o Proof_Context.note_thmss ""
                     (assumes_bindings ~~ map (map (fn th => ([th], []))) premss)));
 
         val _ = Variable.warn_extra_tfrees fix_ctxt goal_ctxt;