Named_Target.theory_init

--- a/src/HOL/Tools/inductive.ML	Thu Aug 12 09:00:19 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Aug 12 13:23:46 2010 +0200
@@ -998,7 +998,7 @@
   let
     val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     val ctxt' = thy
-      |> Named_Target.init NONE
+      |> Named_Target.theory_init
       |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
       |> Local_Theory.exit;
     val info = #2 (the_inductive ctxt' name);

--- a/src/HOL/Tools/primrec.ML	Thu Aug 12 09:00:19 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Thu Aug 12 13:23:46 2010 +0200
@@ -292,7 +292,7 @@
 
 fun add_primrec_global fixes specs thy =
   let
-    val lthy = Named_Target.init NONE thy;
+    val lthy = Named_Target.theory_init thy;
     val ((ts, simps), lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
   in ((ts, simps'), Local_Theory.exit_global lthy') end;

--- a/src/HOL/Tools/typedef.ML	Thu Aug 12 09:00:19 2010 +0200
+++ b/src/HOL/Tools/typedef.ML	Thu Aug 12 13:23:46 2010 +0200
@@ -268,7 +268,7 @@
   in typedef_result inhabited lthy' end;
 
 fun add_typedef_global def opt_name typ set opt_morphs tac =
-  Named_Target.init NONE
+  Named_Target.theory_init
   #> add_typedef def opt_name typ set opt_morphs tac
   #> Local_Theory.exit_result_global (apsnd o transform_info);
 

--- a/src/Pure/Isar/named_target.ML	Thu Aug 12 09:00:19 2010 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu Aug 12 13:23:46 2010 +0200
@@ -9,6 +9,7 @@
 sig
   val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
   val init: string option -> theory -> local_theory
+  val theory_init: theory -> local_theory
   val context_cmd: xstring -> theory -> local_theory
 end;
 
@@ -202,6 +203,8 @@
 
 fun init target thy = init_target (named_target thy target) thy;
 
+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;
 

--- a/src/Pure/Isar/specification.ML	Thu Aug 12 09:00:19 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Aug 12 13:23:46 2010 +0200
@@ -185,7 +185,7 @@
 
     (*facts*)
     val (facts, facts_lthy) = axioms_thy
-      |> Named_Target.init NONE
+      |> Named_Target.theory_init
       |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
       |> Local_Theory.notes axioms;
 

--- a/src/Pure/Isar/toplevel.ML	Thu Aug 12 09:00:19 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Aug 12 13:23:46 2010 +0200
@@ -193,7 +193,7 @@
 
 (* print state *)
 
-val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.init NONE) I;
+val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I;
 
 fun print_state_context state =
   (case try node_of state of

--- a/src/Pure/Isar/typedecl.ML	Thu Aug 12 09:00:19 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML	Thu Aug 12 13:23:46 2010 +0200
@@ -75,7 +75,7 @@
   end;
 
 fun typedecl_global decl =
-  Named_Target.init NONE
+  Named_Target.theory_init
   #> typedecl decl
   #> Local_Theory.exit_result_global Morphism.typ;
 
@@ -115,7 +115,7 @@
 end;
 
 fun abbrev_global decl rhs =
-  Named_Target.init NONE
+  Named_Target.theory_init
   #> abbrev decl rhs
   #> Local_Theory.exit_result_global (K I);