tuned signature;

--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Oct 13 21:41:29 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Oct 13 21:46:41 2014 +0200
@@ -251,8 +251,7 @@
         |> f config type_names
         |> Sign.restore_naming thy));
 
-val interpretation_data =
-  Named_Target.theory_map o Old_Datatype_Plugin.data Plugin_Name.default_filter;
+val interpretation_data = Named_Target.theory_map o Old_Datatype_Plugin.data_default;
 
 
 open Old_Datatype_Aux;

--- a/src/Pure/Isar/code.ML	Mon Oct 13 21:41:29 2014 +0200
+++ b/src/Pure/Isar/code.ML	Mon Oct 13 21:46:41 2014 +0200
@@ -1257,7 +1257,7 @@
   in
     thy
     |> register_type (tyco, (vs, Constructors (cos, [])))
-    |> Named_Target.theory_map (Datatype_Plugin.data Plugin_Name.default_filter tyco)
+    |> Named_Target.theory_map (Datatype_Plugin.data_default tyco)
   end;
 
 fun add_datatype_cmd raw_constrs thy =
@@ -1281,7 +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_map (Abstype_Plugin.data Plugin_Name.default_filter tyco)
+    |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
   end;
 
 

--- a/src/Pure/Tools/plugin.ML	Mon Oct 13 21:41:29 2014 +0200
+++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 21:46:41 2014 +0200
@@ -97,6 +97,7 @@
 sig
   type T
   val data: Plugin_Name.filter -> T -> local_theory -> local_theory
+  val data_default: T -> local_theory -> local_theory
   val interpretation: string -> (T -> local_theory -> local_theory) -> theory -> theory
 end;
 
@@ -178,6 +179,8 @@
     Plugin_Data.map (apfst (cons (mk_data filter (Sign.naming_of thy) x))) thy)
   #> consolidate;
 
+val data_default = data Plugin_Name.default_filter;
+
 fun interpretation name f =
   Plugin_Data.map (apsnd (cons (mk_interp name f, [])))
   #> perhaps consolidate';