diff -r 4e4a4c758f9c -r 50b229a5a097 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Oct 13 20:51:48 2014 +0200
+++ b/src/Pure/Isar/code.ML	Mon Oct 13 21:41:29 2014 +0200
@@ -1257,9 +1257,7 @@
   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 =
@@ -1283,9 +1281,7 @@
     |> 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;