tuned signature;

--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 13 20:51:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 13 21:41:29 2014 +0200
@@ -176,7 +176,7 @@
         set_inducts = []}}
   end;
 
-val _ = Theory.setup (map_local_theory (fn lthy =>
+val _ = Theory.setup (Named_Target.theory_map (fn lthy =>
   fold (BNF_FP_Def_Sugar.register_fp_sugars (K true) o single o (fn f => f lthy))
     [fp_sugar_of_sum, fp_sugar_of_prod] lthy));
 

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Oct 13 20:51:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Oct 13 21:41:29 2014 +0200
@@ -499,7 +499,7 @@
     |> snd
   end;
 
-val datatype_compat_global = map_local_theory o datatype_compat;
+val datatype_compat_global = Named_Target.theory_map o datatype_compat;
 
 fun datatype_compat_cmd raw_fpT_names lthy =
   let
@@ -527,7 +527,8 @@
   in
     (fpT_names,
      thy
-     |> map_local_theory (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs))
+     |> Named_Target.theory_map
+       (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs))
      |> not (member (op =) prefs Keep_Nesting) ? perhaps (try (datatype_compat_global fpT_names)))
   end;
 

--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Oct 13 20:51:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Oct 13 21:41:29 2014 +0200
@@ -103,7 +103,6 @@
   val parse_type_args_named_constrained: (binding option * (string * string option)) list parser
   val parse_map_rel_bindings: (binding * binding) parser
 
-  val map_local_theory: (local_theory -> local_theory) -> theory -> theory
   val typedef: binding * (string * sort) list * mixfix -> term ->
     (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
 end;
@@ -141,8 +140,6 @@
     >> (fn ps => fold extract_map_rel ps no_map_rel)
   || Scan.succeed no_map_rel;
 
-fun map_local_theory f = Named_Target.theory_init #> f #> Local_Theory.exit_global;
-
 fun typedef (b, Ts, mx) set opt_morphs tac lthy =
   let
     (*Work around loss of qualification in "typedef" axioms by replicating it in the name*)

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Oct 13 20:51:48 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Oct 13 21:41:29 2014 +0200
@@ -204,9 +204,7 @@
     else
       thy
       |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
-      |> Named_Target.theory_init
-      |> Ctr_Sugar_Plugin.data plugins ctr_sugar
-      |> Local_Theory.exit_global
+      |> Named_Target.theory_map (Ctr_Sugar_Plugin.data plugins ctr_sugar)
   end;
 
 val isN = "is_";

--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Oct 13 20:51:48 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Oct 13 21:41:29 2014 +0200
@@ -251,10 +251,8 @@
         |> f config type_names
         |> Sign.restore_naming thy));
 
-fun interpretation_data x =
-  Named_Target.theory_init #>
-  Old_Datatype_Plugin.data Plugin_Name.default_filter x #>
-  Local_Theory.exit_global;
+val interpretation_data =
+  Named_Target.theory_map o Old_Datatype_Plugin.data Plugin_Name.default_filter;
 
 
 open Old_Datatype_Aux;

--- 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;
 
 

--- a/src/Pure/Isar/named_target.ML	Mon Oct 13 20:51:48 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Mon Oct 13 21:41:29 2014 +0200
@@ -13,6 +13,7 @@
   val class_of: local_theory -> string option
   val init: string -> theory -> local_theory
   val theory_init: theory -> local_theory
+  val theory_map: (local_theory -> local_theory) -> theory -> theory
   val theory_like_init: (local_theory -> local_theory) -> theory -> local_theory
   val begin: xstring * Position.T -> theory -> local_theory
   val exit: local_theory -> theory
@@ -176,6 +177,8 @@
 
 val theory_init = init "";
 
+fun theory_map f = theory_init #> f #> Local_Theory.exit_global;
+
 fun theory_like_init before_exit = gen_init (SOME before_exit) "";
 
 

--- a/src/Pure/Tools/plugin.ML	Mon Oct 13 20:51:48 2014 +0200
+++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 21:41:29 2014 +0200
@@ -163,10 +163,8 @@
   unfinished_data #> (fn (unfinished, thy) =>
     if forall (null o #2) unfinished then NONE
     else
-      Named_Target.theory_init thy
-      |> fold_rev (fn (interp, data) => fold_rev (apply true interp) data) unfinished
-      |> Local_Theory.exit_global
-      |> SOME);
+      SOME (Named_Target.theory_map
+        (fold_rev (fn (interp, data) => fold_rev (apply true interp) data) unfinished) thy));
 
 end;