diff -r 72a2e33d3b9e -r aad79a127628 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Oct 16 18:55:34 1998 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Oct 16 19:25:58 1998 +0200
@@ -450,7 +450,7 @@
       Theory.add_path (space_implode "_" new_type_names) |>
       PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
-      parent_path flat_names;
+      Theory.parent_path;
 
     val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms