# HG changeset patch
# User haftmann
# Date 1281292885 -7200
# Node ID 12d3a5f04a723ae54041d3a1ea9c07b0b6c825bd
# Parent  130d89f79ac1395f00e77522043e6f084286eec5
unravelled target initialization code

diff -r 130d89f79ac1 -r 12d3a5f04a72 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sun Aug 08 08:39:45 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Sun Aug 08 20:41:25 2010 +0200
@@ -358,50 +358,51 @@
 
 local
 
-fun init_target _ NONE = global_target
-  | init_target thy (SOME target) =
-      if Locale.defined thy target
-      then make_target target true (Class_Target.is_class thy target) ([], [], []) []
-      else error ("No such locale: " ^ quote target);
-
-fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
+fun init_data (Target {target, is_locale, is_class, instantiation, overloading}) =
   if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
   else if not (null overloading) then Overloading.init overloading
   else if not is_locale then ProofContext.init_global
   else if not is_class then Locale.init target
   else Class_Target.init target;
 
-fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
-  Data.put ta #>
-  Local_Theory.init NONE (Long_Name.base_name target)
-   {pretty = pretty ta,
-    abbrev = abbrev ta,
-    define = define ta,
-    notes = notes ta,
-    declaration = declaration ta,
-    syntax_declaration = syntax_declaration ta,
-    reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
-    exit = Local_Theory.target_of o
-      (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
-       else if not (null overloading) then Overloading.conclude
-       else I)}
-and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
+fun init_target (ta as Target {target, instantiation, overloading, ...}) thy =
+  thy
+  |> init_data ta
+  |> Data.put ta
+  |> Local_Theory.init NONE (Long_Name.base_name target)
+     {pretty = pretty ta,
+      abbrev = abbrev ta,
+      define = define ta,
+      notes = notes ta,
+      declaration = declaration ta,
+      syntax_declaration = syntax_declaration ta,
+      reinit = init_target ta o ProofContext.theory_of,
+      exit = Local_Theory.target_of o
+        (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
+         else if not (null overloading) then Overloading.conclude
+         else I)};
+
+fun named_target _ NONE = global_target
+  | named_target thy (SOME target) =
+      if Locale.defined thy target
+      then make_target target true (Class_Target.is_class thy target) ([], [], []) []
+      else error ("No such locale: " ^ quote target);
 
 fun gen_overloading prep_const raw_ops thy =
   let
     val ctxt = ProofContext.init_global thy;
     val ops = raw_ops |> map (fn (name, const, checked) =>
       (name, Term.dest_Const (prep_const ctxt const), checked));
-  in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
+  in thy |> init_target (make_target "" false false ([], [], []) ops) end;
 
 in
 
-fun init target thy = init_lthy_ctxt (init_target thy target) thy;
+fun init target thy = init_target (named_target thy target) thy;
 
 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 arities = init_target (make_target "" false false arities []);
 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);