proper binding position for the resulting definition command, not this source file;
authorwenzelm
Tue Sep 04 22:33:19 2018 +0200 (9 months ago)
changeset 68910a21202dfe3eb
parent 68909 34e777447ed5
child 68912 ecc76fa24a32
proper binding position for the resulting definition command, not this source file;
src/HOL/Library/datatype_records.ML
     1.1 --- a/src/HOL/Library/datatype_records.ML	Thu Aug 30 10:42:42 2018 +0200
     1.2 +++ b/src/HOL/Library/datatype_records.ML	Tue Sep 04 22:33:19 2018 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4      fun mk_name sel =
     1.5        Binding.name ("update_" ^ Long_Name.base_name (fst (dest_Const sel)))
     1.6  
     1.7 -    val thms_binding = (@{binding record_simps}, @{attributes [simp]})
     1.8 +    val thms_binding = (Binding.name "record_simps", @{attributes [simp]})
     1.9  
    1.10      fun mk_t idx =
    1.11        let