src/Pure/Isar/proof.ML

     |-> (fn vars =>
       map_context_result (prep_binds false (map swap raw_rhss))
       #-> (fn rhss =>
         let
           val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
-            ((x, mx), ((Binding.reset_pos (Thm.def_binding_optional x a), atts), rhs)));
+            ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
         in map_context_result (Local_Defs.add_defs defs) end))
     |-> (set_facts o map (#2 o #2))
   end;
 
 in

       map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, export (prove fixes_ctxt th)))
         (defs1 ~~ defs2 ~~ defs3)
       |> unflat (map snd raw_defs);
     val notes =
       map2 (fn ((a, raw_atts), _) => fn def_thms =>
-        ((Binding.reset_pos (Thm.def_binding_optional (Binding.conglomerate (map #1 def_thms)) a),
+        ((Thm.def_binding_optional (Binding.conglomerate (map #1 def_thms)) a,
           map (prep_att defs_ctxt) raw_atts), map (fn (_, th) => ([th], [])) def_thms))
         raw_defs def_thmss;
   in
     state
     |> map_context (K defs_ctxt #> fold Variable.bind_term binds')