src/Pure/Isar/code.ML

     val constrs = map (unoverload_const_typ thy) proto_constrs;
     val (tyco, (vs, cos)) = constrset_of_consts thy constrs;
   in
     thy
     |> register_type (tyco, (vs, Constructors (cos, [])))
-    |> Named_Target.theory_init
-    |> Datatype_Plugin.data Plugin_Name.default_filter tyco
-    |> Local_Theory.exit_global
+    |> Named_Target.theory_map (Datatype_Plugin.data Plugin_Name.default_filter tyco)
   end;
 
 fun add_datatype_cmd raw_constrs thy =
   add_datatype (map (read_bare_const thy) raw_constrs) thy;
 

   in
     thy
     |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
     |> change_fun_spec rep
       (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
-    |> Named_Target.theory_init
-    |> Abstype_Plugin.data Plugin_Name.default_filter tyco
-    |> Local_Theory.exit_global
+    |> Named_Target.theory_map (Abstype_Plugin.data Plugin_Name.default_filter tyco)
   end;
 
 
 (* setup *)