--- 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);