# HG changeset patch
# User haftmann
# Date 1402075186 -7200
# Node ID 2d13bf9ea77b9dd9b9106664270b26bc8ae31385
# Parent  74c81a5b5a340a21803695815b4c610efb295315
dropped obscure and unused ad-hoc before_exit hook for named targets

diff -r 74c81a5b5a34 -r 2d13bf9ea77b src/Doc/Implementation/Local_Theory.thy
--- a/src/Doc/Implementation/Local_Theory.thy	Fri Jun 06 12:36:06 2014 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy	Fri Jun 06 19:19:46 2014 +0200
@@ -96,8 +96,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
-  @{index_ML Named_Target.init: "(local_theory -> local_theory) ->
-    string -> theory -> local_theory"} \\[1ex]
+  @{index_ML Named_Target.init: "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 ->
@@ -120,9 +119,7 @@
   non-empty name refers to a @{command locale} or @{command class}
   context (a fully-qualified internal name is expected here).  This is
   useful for experimentation --- normally the Isar toplevel already
-  takes care to initialize the local theory context.  The given @{text
-  "before_exit"} function is invoked before leaving the context; in
-  most situations plain identity @{ML I} is sufficient.
+  takes care to initialize the local theory context.
 
   \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
   lthy"} defines a local entity according to the specification that is
diff -r 74c81a5b5a34 -r 2d13bf9ea77b src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Fri Jun 06 12:36:06 2014 +0200
+++ b/src/HOL/Statespace/state_space.ML	Fri Jun 06 19:19:46 2014 +0200
@@ -127,20 +127,20 @@
 
 fun prove_interpretation_in ctxt_tac (name, expr) thy =
    thy
-   |> Expression.sublocale_global_cmd I (name, Position.none) (expression_no_pos expr) []
+   |> Expression.sublocale_global_cmd (name, Position.none) (expression_no_pos expr) []
    |> Proof.global_terminal_proof
          ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
    |> Proof_Context.theory_of
 
 fun add_locale name expr elems thy =
   thy
-  |> Expression.add_locale I (Binding.name name) (Binding.name name) expr elems
+  |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
   |> snd
   |> Local_Theory.exit;
 
 fun add_locale_cmd name expr elems thy =
   thy
-  |> Expression.add_locale_cmd I (Binding.name name) Binding.empty (expression_no_pos expr) elems
+  |> Expression.add_locale_cmd (Binding.name name) Binding.empty (expression_no_pos expr) elems
   |> snd
   |> Local_Theory.exit;
 
@@ -294,7 +294,7 @@
 
 fun add_declaration name decl thy =
   thy
-  |> Named_Target.init I name
+  |> Named_Target.init name
   |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy)
   |> Local_Theory.exit_global;
 
diff -r 74c81a5b5a34 -r 2d13bf9ea77b src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Fri Jun 06 12:36:06 2014 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Fri Jun 06 19:19:46 2014 +0200
@@ -6,14 +6,14 @@
 
 signature CLASS_DECLARATION =
 sig
-  val class: (local_theory -> local_theory) -> binding -> class list ->
+  val class: binding -> class list ->
     Element.context_i list -> theory -> string * local_theory
-  val class_cmd: (local_theory -> local_theory) -> binding -> xstring list ->
+  val class_cmd: binding -> xstring list ->
     Element.context list -> theory -> string * local_theory
-  val prove_subclass: (local_theory -> local_theory) -> tactic -> class ->
+  val prove_subclass: tactic -> class ->
     local_theory -> local_theory
-  val subclass: (local_theory -> local_theory) -> class -> local_theory -> Proof.state
-  val subclass_cmd: (local_theory -> local_theory) -> xstring -> local_theory -> Proof.state
+  val subclass: class -> local_theory -> Proof.state
+  val subclass_cmd: xstring -> local_theory -> Proof.state
 end;
 
 structure Class_Declaration: CLASS_DECLARATION =
@@ -306,7 +306,7 @@
     #> pair (param_map, params, assm_axiom)))
   end;
 
-fun gen_class prep_class_spec before_exit b raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
   let
     val class = Sign.full_name thy b;
     val prefix = Binding.qualify true "class";
@@ -314,7 +314,7 @@
       prep_class_spec thy raw_supclasses raw_elems;
   in
     thy
-    |> Expression.add_locale I b (prefix b) supexpr elems
+    |> Expression.add_locale b (prefix b) supexpr elems
     |> snd |> Local_Theory.exit_global
     |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
     |-> (fn (param_map, params, assm_axiom) =>
@@ -325,7 +325,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 before_exit class
+    |> Named_Target.init class
     |> pair class
   end;
 
@@ -342,7 +342,7 @@
 
 local
 
-fun gen_subclass prep_class do_proof before_exit raw_sup lthy =
+fun gen_subclass prep_class do_proof raw_sup lthy =
   let
     val thy = Proof_Context.theory_of lthy;
     val proto_sup = prep_class thy raw_sup;
@@ -371,7 +371,7 @@
 
 in
 
-fun prove_subclass before_exit tac = gen_subclass (K I) (tactic_proof tac) before_exit;
+fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
 
 fun subclass x = gen_subclass (K I) user_proof x;
 fun subclass_cmd x =
diff -r 74c81a5b5a34 -r 2d13bf9ea77b src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Jun 06 12:36:06 2014 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Jun 06 19:19:46 2014 +0200
@@ -31,9 +31,9 @@
   val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
     Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
-  val add_locale: (local_theory -> local_theory) -> binding -> binding ->
+  val add_locale: binding -> binding ->
     expression_i -> Element.context_i list -> theory -> string * local_theory
-  val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding ->
+  val add_locale_cmd: binding -> binding ->
     expression -> Element.context list -> theory -> string * local_theory
 
   (* Interpretation *)
@@ -53,9 +53,9 @@
     local_theory -> Proof.state
   val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
   val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
-  val sublocale_global: (local_theory -> local_theory) -> string -> expression_i ->
+  val sublocale_global: string -> expression_i ->
     (Attrib.binding * term) list -> theory -> Proof.state
-  val sublocale_global_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
+  val sublocale_global_cmd: xstring * Position.T -> expression ->
     (Attrib.binding * string) list -> theory -> Proof.state
 
   (* Diagnostic *)
@@ -762,7 +762,7 @@
   | defines_to_notes _ e = e;
 
 fun gen_add_locale prep_decl
-    before_exit binding raw_predicate_binding raw_import raw_body thy =
+    binding raw_predicate_binding raw_import raw_body thy =
   let
     val name = Sign.full_name thy binding;
     val _ = Locale.defined thy name andalso
@@ -820,7 +820,7 @@
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
-      |> Named_Target.init before_exit name
+      |> Named_Target.init name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
@@ -938,9 +938,9 @@
 (* special case: global sublocale command *)
 
 fun gen_sublocale_global prep_loc prep_interpretation
-    before_exit raw_locale expression raw_eqns thy =
+    raw_locale expression raw_eqns thy =
   let
-    val lthy = Named_Target.init before_exit (prep_loc thy raw_locale) thy;
+    val lthy = Named_Target.init (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 74c81a5b5a34 -r 2d13bf9ea77b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jun 06 12:36:06 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jun 06 19:19:46 2014 +0200
@@ -442,7 +442,7 @@
       Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           Toplevel.begin_local_theory begin
-            (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
+            (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
 
 fun interpretation_args mandatory =
   Parse.!!! (Parse_Spec.locale_expression mandatory) --
@@ -454,7 +454,7 @@
     "prove sublocale relation between a locale and a locale expression"
     ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
       interpretation_args false >> (fn (loc, (expr, equations)) =>
-        Toplevel.theory_to_proof (Expression.sublocale_global_cmd I loc expr equations)))
+        Toplevel.theory_to_proof (Expression.sublocale_global_cmd loc expr equations)))
     || interpretation_args false >> (fn (expr, equations) =>
         Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
 
@@ -483,11 +483,11 @@
    (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
         Toplevel.begin_local_theory begin
-          (Class_Declaration.class_cmd I name supclasses elems #> snd)));
+          (Class_Declaration.class_cmd name supclasses elems #> snd)));
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "subclass"} "prove a subclass relation"
-    (Parse.class >> Class_Declaration.subclass_cmd I);
+    (Parse.class >> Class_Declaration.subclass_cmd);
 
 val _ =
   Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
diff -r 74c81a5b5a34 -r 2d13bf9ea77b src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Fri Jun 06 12:36:06 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Fri Jun 06 19:19:46 2014 +0200
@@ -9,7 +9,7 @@
 sig
   val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
   val is_theory: local_theory -> bool
-  val init: (local_theory -> local_theory) -> string -> theory -> local_theory
+  val init: string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val reinit: local_theory -> local_theory -> local_theory
   val context_cmd: xstring * Position.T -> theory -> local_theory
@@ -21,17 +21,15 @@
 (* context data *)
 
 datatype target =
-  Target of {target: string, is_locale: bool, is_class: bool,
-    before_exit: local_theory -> local_theory};
+  Target of {target: string, is_locale: bool, is_class: bool};
+
+fun make_target target is_locale is_class =
+  Target {target = target, is_locale = is_locale, is_class = is_class};
 
-fun make_target target is_locale is_class before_exit =
-  Target {target = target, is_locale = is_locale, is_class = is_class,
-    before_exit = before_exit};
-
-fun named_target _ "" before_exit = make_target "" false false before_exit
-  | named_target thy target before_exit =
+fun named_target _ "" = make_target "" false false
+  | named_target thy target =
       if Locale.defined thy target
-      then make_target target true (Class.is_class thy target) before_exit
+      then make_target target true (Class.is_class thy target)
       else error ("No such locale: " ^ quote target);
 
 structure Data = Proof_Data
@@ -141,9 +139,9 @@
   else if not is_class then Locale.init target
   else Class.init target;
 
-fun init before_exit target thy =
+fun init target thy =
   let
-    val ta = named_target thy target before_exit;
+    val ta = named_target thy target;
     val naming = Sign.naming_of thy
       |> Name_Space.mandatory_path (Long_Name.base_name target);
   in
@@ -158,16 +156,16 @@
         declaration = declaration ta,
         subscription = subscription ta,
         pretty = pretty ta,
-        exit = before_exit #> Local_Theory.target_of #> Sign.change_end_local}
+        exit = Local_Theory.target_of #> Sign.change_end_local}
   end;
 
-val theory_init = init I "";
+val theory_init = init "";
 
 val reinit =
   Local_Theory.assert_bottom true #> Data.get #> the #>
-  (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
+  (fn Target {target, ...} => Local_Theory.exit_global #> init target);
 
 fun context_cmd ("-", _) thy = theory_init thy
-  | context_cmd target thy = init I (Locale.check thy target) thy;
+  | context_cmd target thy = init (Locale.check thy target) thy;
 
 end;