--- 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;