Named_Target.theory_init
authorhaftmann
Thu Aug 12 13:23:46 2010 +0200 (2010-08-12)
changeset 3838894d5624dd1f7
parent 38386 370712dd4628
child 38389 d7d915bae307
Named_Target.theory_init
src/HOL/Tools/inductive.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/typedef.ML
src/Pure/Isar/named_target.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/toplevel.ML
src/Pure/Isar/typedecl.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Thu Aug 12 09:00:19 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Thu Aug 12 13:23:46 2010 +0200
     1.3 @@ -998,7 +998,7 @@
     1.4    let
     1.5      val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     1.6      val ctxt' = thy
     1.7 -      |> Named_Target.init NONE
     1.8 +      |> Named_Target.theory_init
     1.9        |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
    1.10        |> Local_Theory.exit;
    1.11      val info = #2 (the_inductive ctxt' name);
     2.1 --- a/src/HOL/Tools/primrec.ML	Thu Aug 12 09:00:19 2010 +0200
     2.2 +++ b/src/HOL/Tools/primrec.ML	Thu Aug 12 13:23:46 2010 +0200
     2.3 @@ -292,7 +292,7 @@
     2.4  
     2.5  fun add_primrec_global fixes specs thy =
     2.6    let
     2.7 -    val lthy = Named_Target.init NONE thy;
     2.8 +    val lthy = Named_Target.theory_init thy;
     2.9      val ((ts, simps), lthy') = add_primrec fixes specs lthy;
    2.10      val simps' = ProofContext.export lthy' lthy simps;
    2.11    in ((ts, simps'), Local_Theory.exit_global lthy') end;
     3.1 --- a/src/HOL/Tools/typedef.ML	Thu Aug 12 09:00:19 2010 +0200
     3.2 +++ b/src/HOL/Tools/typedef.ML	Thu Aug 12 13:23:46 2010 +0200
     3.3 @@ -268,7 +268,7 @@
     3.4    in typedef_result inhabited lthy' end;
     3.5  
     3.6  fun add_typedef_global def opt_name typ set opt_morphs tac =
     3.7 -  Named_Target.init NONE
     3.8 +  Named_Target.theory_init
     3.9    #> add_typedef def opt_name typ set opt_morphs tac
    3.10    #> Local_Theory.exit_result_global (apsnd o transform_info);
    3.11  
     4.1 --- a/src/Pure/Isar/named_target.ML	Thu Aug 12 09:00:19 2010 +0200
     4.2 +++ b/src/Pure/Isar/named_target.ML	Thu Aug 12 13:23:46 2010 +0200
     4.3 @@ -9,6 +9,7 @@
     4.4  sig
     4.5    val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
     4.6    val init: string option -> theory -> local_theory
     4.7 +  val theory_init: theory -> local_theory
     4.8    val context_cmd: xstring -> theory -> local_theory
     4.9  end;
    4.10  
    4.11 @@ -202,6 +203,8 @@
    4.12  
    4.13  fun init target thy = init_target (named_target thy target) thy;
    4.14  
    4.15 +val theory_init = init_target global_target;
    4.16 +
    4.17  fun context_cmd "-" thy = init NONE thy
    4.18    | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
    4.19  
     5.1 --- a/src/Pure/Isar/specification.ML	Thu Aug 12 09:00:19 2010 +0200
     5.2 +++ b/src/Pure/Isar/specification.ML	Thu Aug 12 13:23:46 2010 +0200
     5.3 @@ -185,7 +185,7 @@
     5.4  
     5.5      (*facts*)
     5.6      val (facts, facts_lthy) = axioms_thy
     5.7 -      |> Named_Target.init NONE
     5.8 +      |> Named_Target.theory_init
     5.9        |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
    5.10        |> Local_Theory.notes axioms;
    5.11  
     6.1 --- a/src/Pure/Isar/toplevel.ML	Thu Aug 12 09:00:19 2010 +0200
     6.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Aug 12 13:23:46 2010 +0200
     6.3 @@ -193,7 +193,7 @@
     6.4  
     6.5  (* print state *)
     6.6  
     6.7 -val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.init NONE) I;
     6.8 +val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I;
     6.9  
    6.10  fun print_state_context state =
    6.11    (case try node_of state of
     7.1 --- a/src/Pure/Isar/typedecl.ML	Thu Aug 12 09:00:19 2010 +0200
     7.2 +++ b/src/Pure/Isar/typedecl.ML	Thu Aug 12 13:23:46 2010 +0200
     7.3 @@ -75,7 +75,7 @@
     7.4    end;
     7.5  
     7.6  fun typedecl_global decl =
     7.7 -  Named_Target.init NONE
     7.8 +  Named_Target.theory_init
     7.9    #> typedecl decl
    7.10    #> Local_Theory.exit_result_global Morphism.typ;
    7.11  
    7.12 @@ -115,7 +115,7 @@
    7.13  end;
    7.14  
    7.15  fun abbrev_global decl rhs =
    7.16 -  Named_Target.init NONE
    7.17 +  Named_Target.theory_init
    7.18    #> abbrev decl rhs
    7.19    #> Local_Theory.exit_result_global (K I);
    7.20