# HG changeset patch
# User wenzelm
# Date 1467797391 -7200
# Node ID f199837304d7aa9aa27242f672257c10e61e9541
# Parent  249fa34faba26e85a39f0fc24fa678d6f45b0cc1
tuned signature;

diff -r 249fa34faba2 -r f199837304d7 src/Doc/Implementation/Local_Theory.thy
--- a/src/Doc/Implementation/Local_Theory.thy	Tue Jul 05 23:39:49 2016 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy	Wed Jul 06 11:29:51 2016 +0200
@@ -91,7 +91,8 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
-  @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
+  @{index_ML Named_Target.init: "(local_theory -> local_theory) -> string ->
+    theory -> local_theory"} \\[1ex]
   @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory"} \\
   @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
diff -r 249fa34faba2 -r f199837304d7 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Tue Jul 05 23:39:49 2016 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Jul 06 11:29:51 2016 +0200
@@ -298,7 +298,7 @@
 
 fun add_declaration name decl thy =
   thy
-  |> Named_Target.init name
+  |> Named_Target.init NONE name
   |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy)
   |> Local_Theory.exit_global;
 
diff -r 249fa34faba2 -r f199837304d7 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Tue Jul 05 23:39:49 2016 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Wed Jul 06 11:29:51 2016 +0200
@@ -327,7 +327,7 @@
     #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
     #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
     |> snd
-    |> Named_Target.init class
+    |> Named_Target.init NONE class
     |> pair class
   end;
 
diff -r 249fa34faba2 -r f199837304d7 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Jul 05 23:39:49 2016 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Jul 06 11:29:51 2016 +0200
@@ -825,7 +825,7 @@
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
-      |> Named_Target.init name
+      |> Named_Target.init NONE name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
diff -r 249fa34faba2 -r f199837304d7 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Tue Jul 05 23:39:49 2016 +0200
+++ b/src/Pure/Isar/interpretation.ML	Wed Jul 06 11:29:51 2016 +0200
@@ -220,7 +220,7 @@
 fun gen_global_sublocale prep_loc prep_interpretation
     raw_locale expression raw_defs raw_eqns thy =
   let
-    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
+    val lthy = Named_Target.init NONE (prep_loc thy raw_locale) thy;
     fun setup_proof after_qed =
       Element.witness_proof_eqs
         (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
diff -r 249fa34faba2 -r f199837304d7 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Tue Jul 05 23:39:49 2016 +0200
+++ b/src/Pure/Isar/named_target.ML	Wed Jul 06 11:29:51 2016 +0200
@@ -11,14 +11,13 @@
   val locale_of: local_theory -> string option
   val bottom_locale_of: local_theory -> string option
   val class_of: local_theory -> string option
-  val init: string -> theory -> local_theory
+  val init: (local_theory -> local_theory) option -> 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
-  val switch: (xstring * Position.T) option -> Context.generic
-    -> (local_theory -> Context.generic) * local_theory
+  val switch: (xstring * Position.T) option -> Context.generic ->
+    (local_theory -> Context.generic) * local_theory
 end;
 
 structure Named_Target: NAMED_TARGET =
@@ -133,7 +132,7 @@
   | init_context (locale, false) = Locale.init locale
   | init_context (class, true) = Class.init class;
 
-fun gen_init before_exit target thy =
+fun init before_exit target thy =
   let
     val name_data = make_name_data thy target;
     val background_naming =
@@ -155,19 +154,14 @@
           #> Local_Theory.target_of #> Sign.change_end_local}
   end;
 
-val init = gen_init NONE
-
-val theory_init = init "";
-
+val theory_init = init NONE "";
 fun theory_map f = theory_init #> f #> Local_Theory.exit_global;
 
-fun theory_like_init before_exit = gen_init (SOME before_exit) "";
-
 
 (* toplevel interaction *)
 
 fun begin ("-", _) thy = theory_init thy
-  | begin target thy = init (Locale.check thy target) thy;
+  | begin target thy = init NONE (Locale.check thy target) thy;
 
 val exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
 
@@ -178,7 +172,7 @@
   | switch NONE (Context.Proof lthy) =
       (Context.Proof o Local_Theory.reset, lthy)
   | switch (SOME name) (Context.Proof lthy) =
-      (Context.Proof o init (target_of lthy) o exit,
+      (Context.Proof o init NONE (target_of lthy) o exit,
         (begin name o exit o Local_Theory.assert_nonbrittle) lthy);
 
 end;