proper binding position for the resulting definition command, not this source file;

--- a/src/HOL/Library/datatype_records.ML	Thu Aug 30 10:42:42 2018 +0200
+++ b/src/HOL/Library/datatype_records.ML	Tue Sep 04 22:33:19 2018 +0200
@@ -58,7 +58,7 @@
     fun mk_name sel =
       Binding.name ("update_" ^ Long_Name.base_name (fst (dest_Const sel)))
 
-    val thms_binding = (@{binding record_simps}, @{attributes [simp]})
+    val thms_binding = (Binding.name "record_simps", @{attributes [simp]})
 
     fun mk_t idx =
       let