merged

--- a/NEWS	Thu Oct 29 23:27:07 2020 +0000
+++ b/NEWS	Fri Oct 30 10:09:39 2020 +0000
@@ -67,6 +67,8 @@
 
 INCOMPATIBILITY.
 
+* Local_Theory.init replaces Generic_Target.init.  Minor INCOMPATIBILITY.
+
 
 *** HOL ***
 

--- a/src/Pure/Isar/bundle.ML	Thu Oct 29 23:27:07 2020 +0000
+++ b/src/Pure/Isar/bundle.ML	Fri Oct 30 10:09:39 2020 +0000
@@ -172,7 +172,7 @@
 
 fun init binding thy =
   thy
-  |> Generic_Target.init
+  |> Local_Theory.init
      {background_naming = Sign.naming_of thy,
       setup = set_target [] #> Proof_Context.init_global,
       conclude = conclude false binding #> #2}

--- a/src/Pure/Isar/class.ML	Thu Oct 29 23:27:07 2020 +0000
+++ b/src/Pure/Isar/class.ML	Fri Oct 30 10:09:39 2020 +0000
@@ -693,7 +693,7 @@
       | NONE => NONE);
   in
     thy
-    |> Generic_Target.init
+    |> Local_Theory.init
        {background_naming = Sign.naming_of thy,
         setup = Proof_Context.init_global
           #> Instantiation.put (make_instantiation ((tycos, vs, sort), params))

--- a/src/Pure/Isar/generic_target.ML	Thu Oct 29 23:27:07 2020 +0000
+++ b/src/Pure/Isar/generic_target.ML	Fri Oct 30 10:09:39 2020 +0000
@@ -71,11 +71,6 @@
     local_theory -> local_theory
   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
-
-  (*initialisation*)
-  val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
-    conclude: local_theory -> local_theory} ->
-    Local_Theory.operations -> theory -> local_theory
 end
 
 structure Generic_Target: GENERIC_TARGET =
@@ -438,16 +433,4 @@
 
 fun locale_abbrev locale = abbrev (locale_target_abbrev locale);
 
-
-(** initialisation **)
-
-fun init {background_naming, setup, conclude} operations thy =
-  thy
-  |> Sign.change_begin
-  |> setup
-  |> Local_Theory.init
-      {background_naming = background_naming,
-       exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
-      operations;
-
 end;

--- a/src/Pure/Isar/local_theory.ML	Thu Oct 29 23:27:07 2020 +0000
+++ b/src/Pure/Isar/local_theory.ML	Fri Oct 30 10:09:39 2020 +0000
@@ -65,8 +65,8 @@
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
-  val init: {background_naming: Name_Space.naming, exit: local_theory -> Proof.context} ->
-    operations -> Proof.context -> local_theory
+  val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
+    conclude: local_theory -> Proof.context} -> operations -> theory -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
   val exit_global_nonbrittle: local_theory -> theory
@@ -104,14 +104,13 @@
 type lthy =
  {background_naming: Name_Space.naming,
   operations: operations,
-  after_close: local_theory -> local_theory,
-  exit: local_theory -> Proof.context,
+  conclude: Proof.context -> Proof.context,
   brittle: bool,
   target: Proof.context};
 
-fun make_lthy (background_naming, operations, after_close, exit, brittle, target) : lthy =
+fun make_lthy (background_naming, operations, conclude, brittle, target) : lthy =
   {background_naming = background_naming, operations = operations,
-    after_close = after_close, exit = exit, brittle = brittle, target = target};
+    conclude = conclude, brittle = brittle, target = target};
 
 
 (* context data *)
@@ -151,16 +150,16 @@
 
 fun map_top f =
   assert #>
-  Data.map (fn {background_naming, operations, after_close, exit, brittle, target} :: parents =>
-    make_lthy (f (background_naming, operations, after_close, exit, brittle, target)) :: parents);
+  Data.map (fn {background_naming, operations, conclude, brittle, target} :: parents =>
+    make_lthy (f (background_naming, operations, conclude, brittle, target)) :: parents);
 
 fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
 
 fun map_contexts f lthy =
   let val n = level lthy in
     lthy |> (Data.map o map_index)
-      (fn (i, {background_naming, operations, after_close, exit, brittle, target}) =>
-        make_lthy (background_naming, operations, after_close, exit, brittle,
+      (fn (i, {background_naming, operations, conclude, brittle, target}) =>
+        make_lthy (background_naming, operations, conclude, brittle,
           target
           |> Context_Position.set_visible false
           |> f (n - i - 1)
@@ -173,8 +172,8 @@
 
 fun mark_brittle lthy =
   if level lthy = 1 then
-    map_top (fn (background_naming, operations, after_close, exit, _, target) =>
-      (background_naming, operations, after_close, exit, true, target)) lthy
+    map_top (fn (background_naming, operations, conclude, _, target) =>
+      (background_naming, operations, conclude, true, target)) lthy
   else lthy;
 
 fun assert_nonbrittle lthy =
@@ -187,8 +186,8 @@
 val background_naming_of = #background_naming o top_of;
 
 fun map_background_naming f =
-  map_top (fn (background_naming, operations, after_close, exit, brittle, target) =>
-    (f background_naming, operations, after_close, exit, brittle, target));
+  map_top (fn (background_naming, operations, conclude, brittle, target) =>
+    (f background_naming, operations, conclude, brittle, target));
 
 val restore_background_naming = map_background_naming o K o background_naming_of;
 
@@ -353,12 +352,17 @@
 
 (* main target *)
 
-fun init {background_naming, exit} operations target =
-  target |> Data.map
-    (fn [] => [make_lthy (background_naming, operations, I, exit, false, target)]
-      | _ => error "Local theory already initialized");
+fun init_target background_naming conclude operations target =
+  Data.map (K [make_lthy
+    (background_naming, operations, conclude, false, target)]) target
 
-val exit_of = #exit o bottom_of;
+fun init {background_naming, setup, conclude} operations thy =
+  thy
+  |> Sign.change_begin
+  |> setup
+  |> init_target background_naming (conclude #> target_of #> Sign.change_end_local) operations;
+
+val exit_of = #conclude o bottom_of;
 
 fun exit lthy = exit_of lthy (assert_bottom lthy);
 val exit_global = Proof_Context.theory_of o exit;
@@ -385,15 +389,15 @@
     val _ = assert lthy;
     val (scope, target) = Proof_Context.new_scope lthy;
     val entry = make_lthy (background_naming_of lthy, operations_of lthy,
-      Proof_Context.restore_naming lthy, exit_of lthy, true, target);
+      Proof_Context.restore_naming lthy, true, target);
     val lthy' = Data.map (cons entry) target;
   in (scope, lthy') end;
 
 fun end_nested lthy =
   let
     val _ = assert_not_bottom lthy;
-    val ({after_close, ...} :: rest) = Data.get lthy;
-  in lthy |> Data.put rest |> reset |> after_close end;
+    val ({conclude, ...} :: rest) = Data.get lthy;
+  in lthy |> Data.put rest |> reset |> conclude end;
 
 fun end_nested_result decl (x, lthy) =
    let

--- a/src/Pure/Isar/named_target.ML	Thu Oct 29 23:27:07 2020 +0000
+++ b/src/Pure/Isar/named_target.ML	Fri Oct 30 10:09:39 2020 +0000
@@ -12,8 +12,6 @@
   val bottom_locale_of: local_theory -> string option
   val class_of: local_theory -> string option
   val init: string -> theory -> local_theory
-  val init': {setup: local_theory -> local_theory, conclude: local_theory -> local_theory} ->
-    string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val theory_map: (local_theory -> local_theory) -> theory -> theory
   val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->
@@ -117,21 +115,18 @@
   | setup_context (Locale locale) = Locale.init locale
   | setup_context (Class class) = Class.init class;
 
-fun init' {setup, conclude} ident thy =
+fun init ident thy =
   let
     val target = target_of_ident thy ident;
   in
     thy
-    |> Generic_Target.init
+    |> Local_Theory.init
        {background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident),
-        setup = setup_context target #> setup,
-        conclude = conclude}
+        setup = setup_context target #> Data.put (SOME target),
+        conclude = I}
        (operations target)
   end;
 
-fun init ident thy =
-  init' {setup = Data.put (SOME (target_of_ident thy ident)), conclude = I} ident thy;
-
 val theory_init = init "";
 
 fun theory_map g = theory_init #> g #> Local_Theory.exit_global;

--- a/src/Pure/Isar/overloading.ML	Thu Oct 29 23:27:07 2020 +0000
+++ b/src/Pure/Isar/overloading.ML	Fri Oct 30 10:09:39 2020 +0000
@@ -198,7 +198,7 @@
       (Term.dest_Const (prep_const ctxt const), (v, checked)));
   in
     thy
-    |> Generic_Target.init
+    |> Local_Theory.init
        {background_naming = Sign.naming_of thy,
         setup = Proof_Context.init_global
           #> Data.put overloading_spec