# HG changeset patch
# User haftmann
# Date 1281612498 -7200
# Node ID d7d915bae307046ff2ce1357bc6acc17e26e0a07
# Parent  94d5624dd1f7d8f081da8c37bcbfdecb1b1ab3cd
Named_Target.init: empty string represents theory target

diff -r 94d5624dd1f7 -r d7d915bae307 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Aug 12 13:23:46 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Thu Aug 12 13:28:18 2010 +0200
@@ -466,7 +466,7 @@
                 (suffix valuetypesN full_name,(("",false),Expression.Named  []))],[]) fixestate
      |> ProofContext.theory_of 
      |> fold interprete_parent parents
-     |> add_declaration (SOME full_name) (declare_declinfo components')
+     |> add_declaration full_name (declare_declinfo components')
   end;
 
 
diff -r 94d5624dd1f7 -r d7d915bae307 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Thu Aug 12 13:23:46 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Thu Aug 12 13:28:18 2010 +0200
@@ -290,7 +290,7 @@
        Context.theory_map (Locale.add_registration (class, base_morph)
          (Option.map (rpair true) eq_morph) export_morph)
     #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
-    |> Named_Target.init (SOME class)
+    |> Named_Target.init class
     |> pair class
   end;
 
@@ -323,7 +323,7 @@
     fun after_qed some_wit =
       ProofContext.theory (Class.register_subclass (sub, sup)
         some_dep_morph some_wit export)
-      #> ProofContext.theory_of #> Named_Target.init (SOME sub);
+      #> ProofContext.theory_of #> Named_Target.init sub;
   in do_proof after_qed some_prop goal_ctxt end;
 
 fun user_proof after_qed some_prop =
diff -r 94d5624dd1f7 -r d7d915bae307 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Aug 12 13:23:46 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Aug 12 13:28:18 2010 +0200
@@ -775,7 +775,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 (SOME name)
+      |> Named_Target.init name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
@@ -870,7 +870,7 @@
 fun gen_sublocale prep_expr intern raw_target expression thy =
   let
     val target = intern thy raw_target;
-    val target_ctxt = Named_Target.init (SOME target) thy;
+    val target_ctxt = Named_Target.init target thy;
     val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
     fun after_qed witss = ProofContext.theory
       (fold (fn ((dep, morph), wits) => Locale.add_dependency
diff -r 94d5624dd1f7 -r d7d915bae307 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu Aug 12 13:23:46 2010 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu Aug 12 13:28:18 2010 +0200
@@ -8,7 +8,7 @@
 signature NAMED_TARGET =
 sig
   val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
-  val init: string option -> theory -> local_theory
+  val init: string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val context_cmd: xstring -> theory -> local_theory
 end;
@@ -25,8 +25,8 @@
 
 val global_target = Target {target = "", is_locale = false, is_class = false};
 
-fun named_target _ NONE = global_target
-  | named_target thy (SOME locale) =
+fun named_target _ "" = global_target
+  | named_target thy locale =
       if Locale.defined thy locale
       then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale}
       else error ("No such locale: " ^ quote locale);
@@ -205,8 +205,8 @@
 
 val theory_init = init_target global_target;
 
-fun context_cmd "-" thy = init NONE thy
-  | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
+fun context_cmd "-" thy = init "" thy
+  | context_cmd target thy = init (Locale.intern thy target) thy;
 
 end;
 
diff -r 94d5624dd1f7 -r d7d915bae307 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Aug 12 13:23:46 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Aug 12 13:28:18 2010 +0200
@@ -112,8 +112,7 @@
 fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
   | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
   | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => let
-        val target_name = #target (Named_Target.peek lthy);
-        val target = if target_name = "" then NONE else SOME target_name;
+        val target = #target (Named_Target.peek lthy);
       in Context.Proof (Named_Target.init target (loc_exit lthy')) end;