back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;

--- a/src/CCL/Hered.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/CCL/Hered.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -113,7 +113,7 @@
   res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
 
 val HTTgenIs =
-  map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
+  map (mk_genIs (the_context ()) @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
   ["true : HTTgen(R)",
    "false : HTTgen(R)",
    "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",

--- a/src/FOL/simpdata.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/FOL/simpdata.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -133,7 +133,7 @@
 
 (*No simprules, but basic infastructure for simplification*)
 val FOL_basic_ss =
-  Simplifier.theory_context @{theory} empty_ss
+  Simplifier.theory_context (the_context ()) empty_ss
   setsubgoaler asm_simp_tac
   setSSolver (mk_solver "FOL safe" safe_solver)
   setSolver (mk_solver "FOL unsafe" unsafe_solver)

--- a/src/HOL/Divides.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Divides.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -371,7 +371,7 @@
 
 structure CancelDivMod = CancelDivModFun(CancelDivModData);
 
-val cancel_div_mod_proc = Simplifier.simproc @{theory}
+val cancel_div_mod_proc = Simplifier.simproc (the_context ())
   "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
 
 Addsimprocs[cancel_div_mod_proc];

--- a/src/HOL/IntDiv.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/IntDiv.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -279,7 +279,7 @@
 
 in
 
-val cancel_zdiv_zmod_proc = Simplifier.simproc @{theory}
+val cancel_zdiv_zmod_proc = Simplifier.simproc (the_context ())
   "cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc)
 
 end;

--- a/src/HOL/Lambda/WeakNorm.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -430,11 +430,11 @@
 
 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
 val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1));
-val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
+val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
 
 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
 val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
-val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
+val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
 *}
 
 text {*
@@ -505,11 +505,11 @@
 ML {*
 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
 val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
-val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
+val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
 
 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
 val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
-val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
+val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
 *}
 
 end

--- a/src/HOL/List.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/List.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -686,7 +686,7 @@
 in
 
 val list_eq_simproc =
-  Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
+  Simplifier.simproc (the_context ()) "list_eq" ["(xs::'a list) = ys"] (K list_eq);
 
 end;
 

--- a/src/HOL/Matrix/cplex/matrixlp.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Matrix/cplex/matrixlp.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -25,7 +25,7 @@
 
 local
 
-val cert =  cterm_of @{theory}
+val cert =  cterm_of (the_context ())
 
 in
 
@@ -72,7 +72,7 @@
       "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
       "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
       "ComputeNumeral.natnorm"};
-    val computer = PCompute.make Compute.SML @{theory} ths []
+    val computer = PCompute.make Compute.SML (the_context ()) ths []
 in
 
 fun matrix_compute c = hd (PCompute.rewrite computer [c])

--- a/src/HOL/Nominal/nominal_permeq.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -118,7 +118,7 @@
       | _ => NONE
   end
 
-val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app"
+val perm_simproc_app = Simplifier.simproc (the_context ()) "perm_simproc_app"
   ["Nominal.perm pi x"] perm_simproc_app';
 
 (* a simproc that deals with permutation instances in front of functions  *)
@@ -138,7 +138,7 @@
       | _ => NONE
    end
 
-val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun"
+val perm_simproc_fun = Simplifier.simproc (the_context ()) "perm_simproc_fun"
   ["Nominal.perm pi x"] perm_simproc_fun';
 
 (* function for simplyfying permutations *)
@@ -210,7 +210,7 @@
     end
   | _ => NONE);
 
-val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose"
+val perm_compose_simproc = Simplifier.simproc (the_context ()) "perm_compose"
   ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
 
 fun perm_compose_tac ss i = 

--- a/src/HOL/OrderedGroup.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/OrderedGroup.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -1390,7 +1390,7 @@
         if termless_agrp (y, x) then SOME ac2 else NONE
     | solve_add_ac thy _ _ = NONE
 in
-  val add_ac_proc = Simplifier.simproc @{theory}
+  val add_ac_proc = Simplifier.simproc (the_context ())
     "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
 end;
 

--- a/src/HOL/Product_Type.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Product_Type.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -461,8 +461,8 @@
         | NONE => NONE)
   |   eta_proc _ _ = NONE;
 in
-  val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
-  val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
+  val split_beta_proc = Simplifier.simproc (the_context ()) "split_beta" ["split f z"] (K beta_proc);
+  val split_eta_proc = Simplifier.simproc (the_context ()) "split_eta" ["split f"] (K eta_proc);
 end;
 
 Addsimprocs [split_beta_proc, split_eta_proc];

--- a/src/HOL/Tools/metis_tools.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -368,7 +368,7 @@
     end;
 
   (* INFERENCE RULE: REFL *)
-  val refl_x = cterm_of @{theory} (hd (term_vars (prop_of REFL_THM)));
+  val refl_x = cterm_of (the_context ()) (hd (term_vars (prop_of REFL_THM)));
   val refl_idx = 1 + Thm.maxidx_of REFL_THM;
 
   fun refl_inf ctxt t =
@@ -472,14 +472,14 @@
 
   fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
 
-  val equal_imp_fequal' = cnf_th @{theory} (thm"equal_imp_fequal");
-  val fequal_imp_equal' = cnf_th @{theory} (thm"fequal_imp_equal");
+  val equal_imp_fequal' = cnf_th (the_context ()) (thm"equal_imp_fequal");
+  val fequal_imp_equal' = cnf_th (the_context ()) (thm"fequal_imp_equal");
 
-  val comb_I = cnf_th @{theory} ResHolClause.comb_I;
-  val comb_K = cnf_th @{theory} ResHolClause.comb_K;
-  val comb_B = cnf_th @{theory} ResHolClause.comb_B;
-  val comb_C = cnf_th @{theory} ResHolClause.comb_C;
-  val comb_S = cnf_th @{theory} ResHolClause.comb_S;
+  val comb_I = cnf_th (the_context ()) ResHolClause.comb_I;
+  val comb_K = cnf_th (the_context ()) ResHolClause.comb_K;
+  val comb_B = cnf_th (the_context ()) ResHolClause.comb_B;
+  val comb_C = cnf_th (the_context ()) ResHolClause.comb_C;
+  val comb_S = cnf_th (the_context ()) ResHolClause.comb_S;
 
   fun type_ext thy tms =
     let val subs = ResAtp.tfree_classes_of_terms tms

--- a/src/HOL/Tools/numeral.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Tools/numeral.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -40,7 +40,7 @@
 val oneT = Thm.ctyp_of_term one;
 
 val number_of = @{cpat "number_of"};
-val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
+val numberT = Thm.ctyp_of (the_context ()) (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
 
 fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
 

--- a/src/HOL/Tools/res_axioms.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -159,9 +159,9 @@
 
 val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
 
-val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_B}));
-val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_C}));
-val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_S}));
+val [f_B,g_B] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_B}));
+val [g_C,f_C] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_C}));
+val [f_S,g_S] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_S}));
 
 (*FIXME: requires more use of cterm constructors*)
 fun abstract ct =

--- a/src/HOL/Tools/rewrite_hol_proof.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -17,7 +17,7 @@
 open Proofterm;
 
 val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) Symtab.empty true) o
-    Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
+    Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
 
   (** eliminate meta-equality rules **)
 

--- a/src/HOL/arith_data.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/arith_data.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -136,18 +136,18 @@
 (* prepare nat_cancel simprocs *)
 
 val nat_cancel_sums_add =
-  [Simplifier.simproc @{theory} "nateq_cancel_sums"
+  [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
      ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
      (K EqCancelSums.proc),
-   Simplifier.simproc @{theory} "natless_cancel_sums"
+   Simplifier.simproc (the_context ()) "natless_cancel_sums"
      ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
      (K LessCancelSums.proc),
-   Simplifier.simproc @{theory} "natle_cancel_sums"
+   Simplifier.simproc (the_context ()) "natle_cancel_sums"
      ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
      (K LeCancelSums.proc)];
 
 val nat_cancel_sums = nat_cancel_sums_add @
-  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
+  [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
     ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
     (K DiffCancelSums.proc)];
 

--- a/src/HOL/int_arith1.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/int_arith1.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -579,7 +579,7 @@
 end;
 
 val fast_int_arith_simproc =
-  Simplifier.simproc @{theory}
+  Simplifier.simproc (the_context ())
   "fast_int_arith" 
      ["(m::'a::{ordered_idom,number_ring}) < n",
       "(m::'a::{ordered_idom,number_ring}) <= n",

--- a/src/HOL/simpdata.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/simpdata.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -169,7 +169,7 @@
    ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
 
 val HOL_basic_ss =
-  Simplifier.theory_context @{theory} empty_ss
+  Simplifier.theory_context (the_context ()) empty_ss
     setsubgoaler asm_simp_tac
     setSSolver safe_solver
     setSolver unsafe_solver
@@ -184,11 +184,11 @@
   in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
 
 val defALL_regroup =
-  Simplifier.simproc @{theory}
+  Simplifier.simproc (the_context ())
     "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
 
 val defEX_regroup =
-  Simplifier.simproc @{theory}
+  Simplifier.simproc (the_context ())
     "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
 
 

--- a/src/HOLCF/Pcpo.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOLCF/Pcpo.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -209,7 +209,7 @@
       | _ => SOME meta_UU_reorient;
 in
   val UU_reorient_simproc = 
-    Simplifier.simproc @{theory} "UU_reorient_simproc" ["UU=x"] reorient_proc
+    Simplifier.simproc (the_context ()) "UU_reorient_simproc" ["UU=x"] reorient_proc
 end;
 
 Addsimprocs [UU_reorient_simproc];

--- a/src/ZF/Datatype_ZF.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/ZF/Datatype_ZF.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -103,7 +103,7 @@
    handle Match => NONE;
 
 
- val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;
+ val conv = Simplifier.simproc (the_context ()) "data_free" ["(x::i) = y"] proc;
 
 end;
 

--- a/src/ZF/OrdQuant.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/ZF/OrdQuant.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -382,9 +382,9 @@
 
 in
 
-val defREX_regroup = Simplifier.simproc @{theory}
+val defREX_regroup = Simplifier.simproc (the_context ())
   "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
-val defRALL_regroup = Simplifier.simproc @{theory}
+val defRALL_regroup = Simplifier.simproc (the_context ())
   "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
 
 end;