# HG changeset patch
# User wenzelm
# Date 1413229601 -7200
# Node ID 9e34267662674fb1da7de0b712a35b24f0dafa6f
# Parent  50b229a5a0976c22f905eba1ef0acf6318b0ae71
tuned signature;

diff -r 50b229a5a097 -r 9e3426766267 src/HOL/Tools/Old_Datatype/old_datatype_data.ML
--- 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;
diff -r 50b229a5a097 -r 9e3426766267 src/Pure/Isar/code.ML
--- 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;
 
 
diff -r 50b229a5a097 -r 9e3426766267 src/Pure/Tools/plugin.ML
--- 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';