# HG changeset patch
# User wenzelm
# Date 1683743904 -7200
# Node ID c078a33c2dffe1ef2e83905672e987b3116bdb29
# Parent  ce6e3bc34343736df41ba360347c626bfe079dd0
tuned;

diff -r ce6e3bc34343 -r c078a33c2dff src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Wed May 10 20:30:46 2023 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Wed May 10 20:38:24 2023 +0200
@@ -157,8 +157,8 @@
     thy
     |> Sign.add_path (Long_Name.base_name big_rec_name)
     |> Global_Theory.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
-    |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
-    |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
+    |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
+    |> ConstructorsData.map (fold_rev Symtab.update con_pairs)
     |> Sign.parent_path
   end;