# HG changeset patch
# User wenzelm
# Date 1563975684 -7200
# Node ID cafffcb7d383c7523ea17ad2b07e05d57f3bf86d
# Parent  f881efa6be5008754c1dc7214891127e30a50792
avoid duplicate Thm.name_derivation on unnamed PThm nodes ("simps" vs. "case_eqns" and "recursor_eqns");

diff -r f881efa6be50 -r cafffcb7d383 src/ZF/Tools/datatype_package.ML
--- 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,