src/Pure/Isar/proof.ML

       (Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
 
     fun after_local' [[th]] = put_thms false (AutoBind.thisN, SOME [th]);
     fun after_global' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
     val after_qed' = (after_local', after_global');
-    val this_name = ProofContext.full_bname goal_ctxt AutoBind.thisN;
+    val this_name = ProofContext.full_name goal_ctxt (Binding.name AutoBind.thisN);
 
     val result_ctxt =
       state
       |> map_contexts (Variable.declare_term prop)
       |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))