--- 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 ***
--- 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}
*}
--- 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 =
--- 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)
--- 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,
--- 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"
--- 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 => _"}))
--- 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;
--- 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)) #>
--- 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 =
--- 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