# HG changeset patch
# User wenzelm
# Date 1365606167 -7200
# Node ID 532e0ac5a66dd728b4cb6923403a27629ce755b7
# Parent  385ef6706252064d7a213e0e4799fcda2c7865d5
added ML antiquotation @{theory_context};

diff -r 385ef6706252 -r 532e0ac5a66d NEWS
--- a/NEWS	Wed Apr 10 15:30:19 2013 +0200
+++ b/NEWS	Wed Apr 10 17:02:47 2013 +0200
@@ -119,6 +119,9 @@
     Skip_Proof.prove  ~>  Goal.prove_sorry
     Skip_Proof.prove_global  ~>  Goal.prove_sorry_global
 
+* Antiquotation @{theory_context A} is similar to @{theory A}, but
+presents the result as initial Proof.context.
+
 
 *** System ***
 
diff -r 385ef6706252 -r 532e0ac5a66d src/Doc/IsarImplementation/Prelim.thy
--- a/src/Doc/IsarImplementation/Prelim.thy	Wed Apr 10 15:30:19 2013 +0200
+++ b/src/Doc/IsarImplementation/Prelim.thy	Wed Apr 10 17:02:47 2013 +0200
@@ -226,10 +226,13 @@
 text %mlantiq {*
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "theory"} & : & @{text ML_antiquotation} \\
+  @{ML_antiquotation_def "theory_context"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
   @{rail "
   @@{ML_antiquotation theory} nameref?
+  ;
+  @@{ML_antiquotation theory_context} nameref
   "}
 
   \begin{description}
@@ -241,6 +244,10 @@
   theory @{text "A"} of the background theory of the current context
   --- as abstract value.
 
+  \item @{text "@{theory_context A}"} is similar to @{text "@{theory
+  A}"}, but presents the result as initial @{ML_type Proof.context}
+  (see also @{ML Proof_Context.init_global}).
+
   \end{description}
 *}
 
diff -r 385ef6706252 -r 532e0ac5a66d src/HOL/BNF/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Wed Apr 10 15:30:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Wed Apr 10 17:02:47 2013 +0200
@@ -105,7 +105,7 @@
   (rtac uexhaust THEN'
    EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex])]) cases)) 1;
 
-val naked_ctxt = Proof_Context.init_global @{theory HOL};
+val naked_ctxt = @{theory_context HOL};
 
 (* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
 fun mk_split_tac uexhaust cases injectss distinctsss =
diff -r 385ef6706252 -r 532e0ac5a66d src/HOL/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Wed Apr 10 15:30:19 2013 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Wed Apr 10 17:02:47 2013 +0200
@@ -400,7 +400,7 @@
       ==> input_enabled (A||B)"
 apply (unfold input_enabled_def)
 apply (simp add: Let_def inputs_of_par trans_of_par)
-apply (tactic "safe_tac (Proof_Context.init_global @{theory Fun})")
+apply (tactic "safe_tac @{theory_context Fun}")
 apply (simp add: inp_is_act)
 prefer 2
 apply (simp add: inp_is_act)
diff -r 385ef6706252 -r 532e0ac5a66d src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Apr 10 15:30:19 2013 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Apr 10 17:02:47 2013 +0200
@@ -298,7 +298,7 @@
   let val ss = simpset_of ctxt in
     EVERY'[Seq_induct_tac ctxt sch defs,
            asm_full_simp_tac ss,
-           SELECT_GOAL (safe_tac (Proof_Context.init_global @{theory Fun})),
+           SELECT_GOAL (safe_tac @{theory_context Fun}),
            Seq_case_simp_tac ctxt exA,
            Seq_case_simp_tac ctxt exB,
            asm_full_simp_tac ss,
diff -r 385ef6706252 -r 532e0ac5a66d src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Apr 10 15:30:19 2013 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Apr 10 17:02:47 2013 +0200
@@ -200,7 +200,7 @@
 apply( simp_all)
 apply( tactic "ALLGOALS (REPEAT o resolve_tac [impI, allI])")
 apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
-                 THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *})
+                 THEN_ALL_NEW (full_simp_tac (simpset_of @{theory_context Conform}))) *})
 apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
 
 -- "Level 7"
diff -r 385ef6706252 -r 532e0ac5a66d src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Wed Apr 10 15:30:19 2013 +0200
+++ b/src/HOL/Word/WordBitwise.thy	Wed Apr 10 17:02:47 2013 +0200
@@ -501,7 +501,7 @@
 
 structure Word_Bitwise_Tac = struct
 
-val word_ss = global_simpset_of @{theory Word};
+val word_ss = simpset_of @{theory_context Word};
 
 fun mk_nat_clist ns = List.foldr
   (uncurry (Thm.mk_binop @{cterm "Cons :: nat => _"}))
diff -r 385ef6706252 -r 532e0ac5a66d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 10 15:30:19 2013 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 10 17:02:47 2013 +0200
@@ -10,6 +10,7 @@
 sig
   val theory_of: Proof.context -> theory
   val init_global: theory -> Proof.context
+  val get_global: theory -> string -> Proof.context
   type mode
   val mode_default: mode
   val mode_stmt: mode
@@ -166,6 +167,7 @@
 
 val theory_of = Proof_Context.theory_of;
 val init_global = Proof_Context.init_global;
+val get_global = Proof_Context.get_global;
 
 
 
diff -r 385ef6706252 -r 532e0ac5a66d src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Wed Apr 10 15:30:19 2013 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Apr 10 17:02:47 2013 +0200
@@ -76,6 +76,12 @@
         "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
     || Scan.succeed "Proof_Context.theory_of ML_context") #>
 
+  value (Binding.name "theory_context")
+    (Args.theory -- Scan.lift (Parse.position Args.name) >> (fn (thy, (name, pos)) =>
+      (Position.report pos (Theory.get_markup (Context.get_theory thy name));
+        "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
+        ML_Syntax.print_string name))) #>
+
   inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
 
   inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
diff -r 385ef6706252 -r 532e0ac5a66d src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Apr 10 15:30:19 2013 +0200
+++ b/src/Pure/context.ML	Wed Apr 10 17:02:47 2013 +0200
@@ -21,6 +21,7 @@
   sig
     val theory_of: Proof.context -> theory
     val init_global: theory -> Proof.context
+    val get_global: theory -> string -> Proof.context
   end
 end;
 
@@ -504,6 +505,7 @@
 struct
   val theory_of = theory_of_proof;
   fun init_global thy = Proof.Context (init_data thy, check_thy thy);
+  fun get_global thy name = init_global (get_theory thy name);
 end;
 
 structure Proof_Data =
diff -r 385ef6706252 -r 532e0ac5a66d src/ZF/IntDiv_ZF.thy
--- a/src/ZF/IntDiv_ZF.thy	Wed Apr 10 15:30:19 2013 +0200
+++ b/src/ZF/IntDiv_ZF.thy	Wed Apr 10 17:02:47 2013 +0200
@@ -1712,7 +1712,7 @@
            (if ~b | #0 $<= integ_of w
             then integ_of v zdiv (integ_of w)
             else (integ_of v $+ #1) zdiv (integ_of w))"
- apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT)
+ apply (simp_tac (simpset_of @{theory_context Int} add: zadd_assoc integ_of_BIT)
  apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zdiv_zmult_zmult1 pos_zdiv_mult_2 lemma neg_zdiv_mult_2)
  done
 
@@ -1758,7 +1758,7 @@
                  then #2 $* (integ_of v zmod integ_of w) $+ #1
                  else #2 $* ((integ_of v $+ #1) zmod integ_of w) - #1
             else #2 $* (integ_of v zmod integ_of w))"
- apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT)
+ apply (simp_tac (simpset_of @{theory_context Int} add: zadd_assoc integ_of_BIT)
  apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zmod_zmult_zmult1 pos_zmod_mult_2 lemma neg_zmod_mult_2)
  done