# HG changeset patch
# User haftmann
# Date 1603995808 0
# Node ID 17dc99589a9114c093cc11447a695c06021740fb
# Parent  c7038c397ae38a1d70b2f2cc684a67856b1669be
unified Local_Theory.init with Generic_Target.init

diff -r c7038c397ae3 -r 17dc99589a91 NEWS
--- a/NEWS	Thu Oct 29 10:03:03 2020 +0000
+++ b/NEWS	Thu Oct 29 18:23:28 2020 +0000
@@ -67,6 +67,8 @@
 
 INCOMPATIBILITY.
 
+* Local_Theory.init replaces Generic_Target.init.  Minor INCOMPATIBILITY.
+
 
 *** HOL ***
 
diff -r c7038c397ae3 -r 17dc99589a91 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Thu Oct 29 10:03:03 2020 +0000
+++ b/src/Pure/Isar/bundle.ML	Thu Oct 29 18:23:28 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}
diff -r c7038c397ae3 -r 17dc99589a91 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Oct 29 10:03:03 2020 +0000
+++ b/src/Pure/Isar/class.ML	Thu Oct 29 18:23:28 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))
diff -r c7038c397ae3 -r 17dc99589a91 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Oct 29 10:03:03 2020 +0000
+++ b/src/Pure/Isar/generic_target.ML	Thu Oct 29 18:23:28 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;
diff -r c7038c397ae3 -r 17dc99589a91 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Oct 29 10:03:03 2020 +0000
+++ b/src/Pure/Isar/local_theory.ML	Thu Oct 29 18:23:28 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
@@ -353,10 +353,15 @@
 
 (* 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 exit operations target =
+  Data.map (K [make_lthy (background_naming, operations, I,
+    exit, false, target)]) target
+
+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 = #exit o bottom_of;
 
diff -r c7038c397ae3 -r 17dc99589a91 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu Oct 29 10:03:03 2020 +0000
+++ b/src/Pure/Isar/named_target.ML	Thu Oct 29 18:23:28 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;
diff -r c7038c397ae3 -r 17dc99589a91 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Thu Oct 29 10:03:03 2020 +0000
+++ b/src/Pure/Isar/overloading.ML	Thu Oct 29 18:23:28 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