# HG changeset patch
# User haftmann
# Date 1402121763 -7200
# Node ID 56f3351cc492d3580ef000b38bc68df4b74a7b20
# Parent  766e7f50c22f3264838df352cb4ff56406082e1a
avoid odd Named_Target.reinit altogether

diff -r 766e7f50c22f -r 56f3351cc492 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sat Jun 07 08:16:03 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Sat Jun 07 08:16:03 2014 +0200
@@ -12,7 +12,6 @@
   val class_of: local_theory -> string option
   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
 end;
 
@@ -171,10 +170,6 @@
 
 val theory_init = init "";
 
-val reinit =
-  Local_Theory.assert_bottom true #> Data.get #> the #>
-  (fn Target {target, ...} => Local_Theory.exit_global #> init target);
-
 fun context_cmd ("-", _) thy = theory_init thy
   | context_cmd target thy = init (Locale.check thy target) thy;
 
diff -r 766e7f50c22f -r 56f3351cc492 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Jun 07 08:16:03 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Jun 07 08:16:03 2014 +0200
@@ -115,8 +115,8 @@
   | named_begin NONE (Context.Proof lthy) =
       (Context.Proof o Local_Theory.restore, lthy)
   | named_begin (SOME loc) (Context.Proof lthy) =
-      (Context.Proof o Named_Target.reinit lthy,
-        named_init loc (named_exit (Local_Theory.assert_nonbrittle lthy)));
+      (Context.Proof o Named_Target.init (the (Named_Target.locale_of lthy)) o named_exit,
+        (named_init loc o named_exit o Local_Theory.assert_nonbrittle) lthy);
 
 
 (* datatype node *)