# HG changeset patch
# User wenzelm
# Date 1266532861 -3600
# Node ID 611b90bb89bc10c55bfc9571460296ac1273d4cf
# Parent  214ec053128e2d845bc6746f259abcf92a3be9d6
removed unused Theory_Target.begin;
Theory_Target.init: removed Locale.intern, which was accidentally introduced in 40b3630b0deb;
renamed Theory_Target.context to Theory_Target.context_cmd to emphasize that this involves Locale.intern;
tuned;

diff -r 214ec053128e -r 611b90bb89bc src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Feb 18 23:38:33 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Feb 18 23:41:01 2010 +0100
@@ -390,7 +390,7 @@
 val _ =
   OuterSyntax.command "context" "enter local theory context" K.thy_decl
     (P.name --| P.begin >> (fn name =>
-      Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context name)));
+      Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name)));
 
 
 (* locales *)
diff -r 214ec053128e -r 611b90bb89bc src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Feb 18 23:38:33 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Feb 18 23:41:01 2010 +0100
@@ -7,12 +7,14 @@
 
 signature THEORY_TARGET =
 sig
-  val peek: local_theory -> {target: string, is_locale: bool,
-    is_class: bool, instantiation: string list * (string * sort) list * sort,
+  val peek: local_theory ->
+   {target: string,
+    is_locale: bool,
+    is_class: bool,
+    instantiation: string list * (string * sort) list * sort,
     overloading: (string * (string * typ) * bool) list}
   val init: string option -> theory -> local_theory
-  val begin: string -> Proof.context -> local_theory
-  val context: xstring -> theory -> local_theory
+  val context_cmd: xstring -> theory -> local_theory
   val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
   val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
   val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
@@ -305,13 +307,13 @@
   in ((lhs, (res_name, res)), lthy4) end;
 
 
-(* init *)
+(* init various targets *)
 
 local
 
 fun init_target _ NONE = global_target
   | init_target thy (SOME target) =
-      if Locale.defined thy (Locale.intern thy target)
+      if Locale.defined thy target
       then make_target target true (Class_Target.is_class thy target) ([], [], []) []
       else error ("No such locale: " ^ quote target);
 
@@ -349,17 +351,12 @@
 in
 
 fun init target thy = init_lthy_ctxt (init_target thy target) thy;
-fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
 
-fun context "-" thy = init NONE thy
-  | context target thy = init (SOME (Locale.intern thy target)) thy;
-
-
-(* other targets *)
+fun context_cmd "-" thy = init NONE thy
+  | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
 
 fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
-fun instantiation_cmd raw_arities thy =
-  instantiation (Class_Target.read_multi_arity thy raw_arities) thy;
+fun instantiation_cmd arities thy = instantiation (Class_Target.read_multi_arity thy arities) thy;
 
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
 val overloading_cmd = gen_overloading Syntax.read_term;
diff -r 214ec053128e -r 611b90bb89bc src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Feb 18 23:38:33 2010 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Feb 18 23:41:01 2010 +0100
@@ -104,7 +104,7 @@
 
 type generic_theory = Context.generic;    (*theory or local_theory*)
 
-val loc_init = Theory_Target.context;
+val loc_init = Theory_Target.context_cmd;
 val loc_exit = Local_Theory.exit_global;
 
 fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy