avoid duplicate Thm.name_derivation on unnamed PThm nodes ("simps" vs. "case_eqns" and "recursor_eqns");

--- a/src/ZF/Tools/datatype_package.ML	Wed Jul 24 13:30:15 2019 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Wed Jul 24 15:41:24 2019 +0200
@@ -353,8 +353,6 @@
           fast_tac (put_claset ZF_cs ctxt' addSEs free_SEs @ Su.free_SEs) 1])
     end;
 
-  val simps = case_eqns @ recursor_eqns;
-
   val dt_info =
         {inductive = true,
          constructors = constructors,
@@ -379,13 +377,15 @@
   (*Updating theory components: simprules and datatype info*)
   (thy1 |> Sign.add_path big_rec_base_name
         |> Global_Theory.add_thmss
-         [((Binding.name "simps", simps), [Simplifier.simp_add]),
+         [((Binding.name "case_eqns", case_eqns), []),
+          ((Binding.name "recursor_eqns", recursor_eqns), []),
           ((Binding.empty, intrs), [Cla.safe_intro NONE]),
           ((Binding.name "con_defs", con_defs), []),
-          ((Binding.name "case_eqns", case_eqns), []),
-          ((Binding.name "recursor_eqns", recursor_eqns), []),
           ((Binding.name "free_iffs", free_iffs), []),
-          ((Binding.name "free_elims", free_SEs), [])] |> snd
+          ((Binding.name "free_elims", free_SEs), [])]
+        |-> (fn simps1 :: simps2 :: _ =>
+            Global_Theory.add_thmss
+              [((Binding.name "simps", simps1 @ simps2), [Simplifier.simp_add])]) |> #2
         |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
         |> ConstructorsData.map (fold Symtab.update con_pairs)
         |> Sign.parent_path,