# HG changeset patch
# User haftmann
# Date 1281534315 -7200
# Node ID 0b6fa86110e7b7e1fc4e08d367e517aa6646315e
# Parent  2dfd8b7b8274fd72b3798afb60f9aeb68785de9a
tuned

diff -r 2dfd8b7b8274 -r 0b6fa86110e7 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Aug 11 15:09:31 2010 +0200
+++ b/src/Pure/Isar/named_target.ML	Wed Aug 11 15:45:15 2010 +0200
@@ -22,7 +22,13 @@
 fun make_target target is_locale is_class =
   Target {target = target, is_locale = is_locale, is_class = is_class};
 
-val global_target = make_target "" false false;
+val global_target = Target {target = "", is_locale = false, is_class = false};
+
+fun named_target _ NONE = global_target
+  | named_target thy (SOME locale) =
+      if Locale.defined thy locale
+      then Target {target = locale, is_locale = true, is_class = Class_Target.is_class thy locale}
+      else error ("No such locale: " ^ quote locale);
 
 structure Data = Proof_Data
 (
@@ -168,18 +174,18 @@
     pretty_thy ctxt target is_class;
 
 
-(* init various targets *)
+(* init *)
 
 local
 
-fun init_data (Target {target, is_locale, is_class}) =
+fun init_context (Target {target, is_locale, is_class}) =
   if not is_locale then ProofContext.init_global
   else if not is_class then Locale.init target
   else Class_Target.init target;
 
 fun init_target (ta as Target {target, ...}) thy =
   thy
-  |> init_data ta
+  |> init_context ta
   |> Data.put ta
   |> Local_Theory.init NONE (Long_Name.base_name target)
      {define = Generic_Target.define (target_foundation ta),
@@ -193,12 +199,6 @@
       reinit = init_target ta o ProofContext.theory_of,
       exit = Local_Theory.target_of};
 
-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);
-
 in
 
 fun init target thy = init_target (named_target thy target) thy;