back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
authorwenzelm
Wed Sep 17 21:27:08 2008 +0200 (2008-09-17)
changeset 28262aa7ca36d67fd
parent 28261 045187fc7840
child 28263 69eaa97e7e96
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
src/CCL/Hered.thy
src/FOL/simpdata.ML
src/HOL/Divides.thy
src/HOL/IntDiv.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/List.thy
src/HOL/Matrix/cplex/matrixlp.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/OrderedGroup.thy
src/HOL/Product_Type.thy
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/rewrite_hol_proof.ML
src/HOL/arith_data.ML
src/HOL/int_arith1.ML
src/HOL/simpdata.ML
src/HOLCF/Pcpo.thy
src/ZF/Datatype_ZF.thy
src/ZF/OrdQuant.thy
     1.1 --- a/src/CCL/Hered.thy	Wed Sep 17 21:27:03 2008 +0200
     1.2 +++ b/src/CCL/Hered.thy	Wed Sep 17 21:27:08 2008 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4    res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
     1.5  
     1.6  val HTTgenIs =
     1.7 -  map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
     1.8 +  map (mk_genIs (the_context ()) @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
     1.9    ["true : HTTgen(R)",
    1.10     "false : HTTgen(R)",
    1.11     "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
     2.1 --- a/src/FOL/simpdata.ML	Wed Sep 17 21:27:03 2008 +0200
     2.2 +++ b/src/FOL/simpdata.ML	Wed Sep 17 21:27:08 2008 +0200
     2.3 @@ -133,7 +133,7 @@
     2.4  
     2.5  (*No simprules, but basic infastructure for simplification*)
     2.6  val FOL_basic_ss =
     2.7 -  Simplifier.theory_context @{theory} empty_ss
     2.8 +  Simplifier.theory_context (the_context ()) empty_ss
     2.9    setsubgoaler asm_simp_tac
    2.10    setSSolver (mk_solver "FOL safe" safe_solver)
    2.11    setSolver (mk_solver "FOL unsafe" unsafe_solver)
     3.1 --- a/src/HOL/Divides.thy	Wed Sep 17 21:27:03 2008 +0200
     3.2 +++ b/src/HOL/Divides.thy	Wed Sep 17 21:27:08 2008 +0200
     3.3 @@ -371,7 +371,7 @@
     3.4  
     3.5  structure CancelDivMod = CancelDivModFun(CancelDivModData);
     3.6  
     3.7 -val cancel_div_mod_proc = Simplifier.simproc @{theory}
     3.8 +val cancel_div_mod_proc = Simplifier.simproc (the_context ())
     3.9    "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
    3.10  
    3.11  Addsimprocs[cancel_div_mod_proc];
     4.1 --- a/src/HOL/IntDiv.thy	Wed Sep 17 21:27:03 2008 +0200
     4.2 +++ b/src/HOL/IntDiv.thy	Wed Sep 17 21:27:08 2008 +0200
     4.3 @@ -279,7 +279,7 @@
     4.4  
     4.5  in
     4.6  
     4.7 -val cancel_zdiv_zmod_proc = Simplifier.simproc @{theory}
     4.8 +val cancel_zdiv_zmod_proc = Simplifier.simproc (the_context ())
     4.9    "cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc)
    4.10  
    4.11  end;
     5.1 --- a/src/HOL/Lambda/WeakNorm.thy	Wed Sep 17 21:27:03 2008 +0200
     5.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Wed Sep 17 21:27:08 2008 +0200
     5.3 @@ -430,11 +430,11 @@
     5.4  
     5.5  val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
     5.6  val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1));
     5.7 -val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
     5.8 +val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
     5.9  
    5.10  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)))))"};
    5.11  val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
    5.12 -val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
    5.13 +val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
    5.14  *}
    5.15  
    5.16  text {*
    5.17 @@ -505,11 +505,11 @@
    5.18  ML {*
    5.19  val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
    5.20  val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
    5.21 -val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
    5.22 +val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
    5.23  
    5.24  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)))))"};
    5.25  val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
    5.26 -val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
    5.27 +val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
    5.28  *}
    5.29  
    5.30  end
     6.1 --- a/src/HOL/List.thy	Wed Sep 17 21:27:03 2008 +0200
     6.2 +++ b/src/HOL/List.thy	Wed Sep 17 21:27:08 2008 +0200
     6.3 @@ -686,7 +686,7 @@
     6.4  in
     6.5  
     6.6  val list_eq_simproc =
     6.7 -  Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
     6.8 +  Simplifier.simproc (the_context ()) "list_eq" ["(xs::'a list) = ys"] (K list_eq);
     6.9  
    6.10  end;
    6.11  
     7.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML	Wed Sep 17 21:27:03 2008 +0200
     7.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML	Wed Sep 17 21:27:08 2008 +0200
     7.3 @@ -25,7 +25,7 @@
     7.4  
     7.5  local
     7.6  
     7.7 -val cert =  cterm_of @{theory}
     7.8 +val cert =  cterm_of (the_context ())
     7.9  
    7.10  in
    7.11  
    7.12 @@ -72,7 +72,7 @@
    7.13        "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
    7.14        "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
    7.15        "ComputeNumeral.natnorm"};
    7.16 -    val computer = PCompute.make Compute.SML @{theory} ths []
    7.17 +    val computer = PCompute.make Compute.SML (the_context ()) ths []
    7.18  in
    7.19  
    7.20  fun matrix_compute c = hd (PCompute.rewrite computer [c])
     8.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Sep 17 21:27:03 2008 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Sep 17 21:27:08 2008 +0200
     8.3 @@ -118,7 +118,7 @@
     8.4        | _ => NONE
     8.5    end
     8.6  
     8.7 -val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app"
     8.8 +val perm_simproc_app = Simplifier.simproc (the_context ()) "perm_simproc_app"
     8.9    ["Nominal.perm pi x"] perm_simproc_app';
    8.10  
    8.11  (* a simproc that deals with permutation instances in front of functions  *)
    8.12 @@ -138,7 +138,7 @@
    8.13        | _ => NONE
    8.14     end
    8.15  
    8.16 -val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun"
    8.17 +val perm_simproc_fun = Simplifier.simproc (the_context ()) "perm_simproc_fun"
    8.18    ["Nominal.perm pi x"] perm_simproc_fun';
    8.19  
    8.20  (* function for simplyfying permutations *)
    8.21 @@ -210,7 +210,7 @@
    8.22      end
    8.23    | _ => NONE);
    8.24  
    8.25 -val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose"
    8.26 +val perm_compose_simproc = Simplifier.simproc (the_context ()) "perm_compose"
    8.27    ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
    8.28  
    8.29  fun perm_compose_tac ss i = 
     9.1 --- a/src/HOL/OrderedGroup.thy	Wed Sep 17 21:27:03 2008 +0200
     9.2 +++ b/src/HOL/OrderedGroup.thy	Wed Sep 17 21:27:08 2008 +0200
     9.3 @@ -1390,7 +1390,7 @@
     9.4          if termless_agrp (y, x) then SOME ac2 else NONE
     9.5      | solve_add_ac thy _ _ = NONE
     9.6  in
     9.7 -  val add_ac_proc = Simplifier.simproc @{theory}
     9.8 +  val add_ac_proc = Simplifier.simproc (the_context ())
     9.9      "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
    9.10  end;
    9.11  
    10.1 --- a/src/HOL/Product_Type.thy	Wed Sep 17 21:27:03 2008 +0200
    10.2 +++ b/src/HOL/Product_Type.thy	Wed Sep 17 21:27:08 2008 +0200
    10.3 @@ -461,8 +461,8 @@
    10.4          | NONE => NONE)
    10.5    |   eta_proc _ _ = NONE;
    10.6  in
    10.7 -  val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
    10.8 -  val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
    10.9 +  val split_beta_proc = Simplifier.simproc (the_context ()) "split_beta" ["split f z"] (K beta_proc);
   10.10 +  val split_eta_proc = Simplifier.simproc (the_context ()) "split_eta" ["split f"] (K eta_proc);
   10.11  end;
   10.12  
   10.13  Addsimprocs [split_beta_proc, split_eta_proc];
    11.1 --- a/src/HOL/Tools/metis_tools.ML	Wed Sep 17 21:27:03 2008 +0200
    11.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Sep 17 21:27:08 2008 +0200
    11.3 @@ -368,7 +368,7 @@
    11.4      end;
    11.5  
    11.6    (* INFERENCE RULE: REFL *)
    11.7 -  val refl_x = cterm_of @{theory} (hd (term_vars (prop_of REFL_THM)));
    11.8 +  val refl_x = cterm_of (the_context ()) (hd (term_vars (prop_of REFL_THM)));
    11.9    val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   11.10  
   11.11    fun refl_inf ctxt t =
   11.12 @@ -472,14 +472,14 @@
   11.13  
   11.14    fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
   11.15  
   11.16 -  val equal_imp_fequal' = cnf_th @{theory} (thm"equal_imp_fequal");
   11.17 -  val fequal_imp_equal' = cnf_th @{theory} (thm"fequal_imp_equal");
   11.18 +  val equal_imp_fequal' = cnf_th (the_context ()) (thm"equal_imp_fequal");
   11.19 +  val fequal_imp_equal' = cnf_th (the_context ()) (thm"fequal_imp_equal");
   11.20  
   11.21 -  val comb_I = cnf_th @{theory} ResHolClause.comb_I;
   11.22 -  val comb_K = cnf_th @{theory} ResHolClause.comb_K;
   11.23 -  val comb_B = cnf_th @{theory} ResHolClause.comb_B;
   11.24 -  val comb_C = cnf_th @{theory} ResHolClause.comb_C;
   11.25 -  val comb_S = cnf_th @{theory} ResHolClause.comb_S;
   11.26 +  val comb_I = cnf_th (the_context ()) ResHolClause.comb_I;
   11.27 +  val comb_K = cnf_th (the_context ()) ResHolClause.comb_K;
   11.28 +  val comb_B = cnf_th (the_context ()) ResHolClause.comb_B;
   11.29 +  val comb_C = cnf_th (the_context ()) ResHolClause.comb_C;
   11.30 +  val comb_S = cnf_th (the_context ()) ResHolClause.comb_S;
   11.31  
   11.32    fun type_ext thy tms =
   11.33      let val subs = ResAtp.tfree_classes_of_terms tms
    12.1 --- a/src/HOL/Tools/numeral.ML	Wed Sep 17 21:27:03 2008 +0200
    12.2 +++ b/src/HOL/Tools/numeral.ML	Wed Sep 17 21:27:08 2008 +0200
    12.3 @@ -40,7 +40,7 @@
    12.4  val oneT = Thm.ctyp_of_term one;
    12.5  
    12.6  val number_of = @{cpat "number_of"};
    12.7 -val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
    12.8 +val numberT = Thm.ctyp_of (the_context ()) (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
    12.9  
   12.10  fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
   12.11  
    13.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Sep 17 21:27:03 2008 +0200
    13.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Sep 17 21:27:08 2008 +0200
    13.3 @@ -159,9 +159,9 @@
    13.4  
    13.5  val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
    13.6  
    13.7 -val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_B}));
    13.8 -val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_C}));
    13.9 -val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_S}));
   13.10 +val [f_B,g_B] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_B}));
   13.11 +val [g_C,f_C] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_C}));
   13.12 +val [f_S,g_S] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_S}));
   13.13  
   13.14  (*FIXME: requires more use of cterm constructors*)
   13.15  fun abstract ct =
    14.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Wed Sep 17 21:27:03 2008 +0200
    14.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Wed Sep 17 21:27:08 2008 +0200
    14.3 @@ -17,7 +17,7 @@
    14.4  open Proofterm;
    14.5  
    14.6  val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) Symtab.empty true) o
    14.7 -    Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
    14.8 +    Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
    14.9  
   14.10    (** eliminate meta-equality rules **)
   14.11  
    15.1 --- a/src/HOL/arith_data.ML	Wed Sep 17 21:27:03 2008 +0200
    15.2 +++ b/src/HOL/arith_data.ML	Wed Sep 17 21:27:08 2008 +0200
    15.3 @@ -136,18 +136,18 @@
    15.4  (* prepare nat_cancel simprocs *)
    15.5  
    15.6  val nat_cancel_sums_add =
    15.7 -  [Simplifier.simproc @{theory} "nateq_cancel_sums"
    15.8 +  [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
    15.9       ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
   15.10       (K EqCancelSums.proc),
   15.11 -   Simplifier.simproc @{theory} "natless_cancel_sums"
   15.12 +   Simplifier.simproc (the_context ()) "natless_cancel_sums"
   15.13       ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
   15.14       (K LessCancelSums.proc),
   15.15 -   Simplifier.simproc @{theory} "natle_cancel_sums"
   15.16 +   Simplifier.simproc (the_context ()) "natle_cancel_sums"
   15.17       ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
   15.18       (K LeCancelSums.proc)];
   15.19  
   15.20  val nat_cancel_sums = nat_cancel_sums_add @
   15.21 -  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
   15.22 +  [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
   15.23      ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
   15.24      (K DiffCancelSums.proc)];
   15.25  
    16.1 --- a/src/HOL/int_arith1.ML	Wed Sep 17 21:27:03 2008 +0200
    16.2 +++ b/src/HOL/int_arith1.ML	Wed Sep 17 21:27:08 2008 +0200
    16.3 @@ -579,7 +579,7 @@
    16.4  end;
    16.5  
    16.6  val fast_int_arith_simproc =
    16.7 -  Simplifier.simproc @{theory}
    16.8 +  Simplifier.simproc (the_context ())
    16.9    "fast_int_arith" 
   16.10       ["(m::'a::{ordered_idom,number_ring}) < n",
   16.11        "(m::'a::{ordered_idom,number_ring}) <= n",
    17.1 --- a/src/HOL/simpdata.ML	Wed Sep 17 21:27:03 2008 +0200
    17.2 +++ b/src/HOL/simpdata.ML	Wed Sep 17 21:27:08 2008 +0200
    17.3 @@ -169,7 +169,7 @@
    17.4     ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
    17.5  
    17.6  val HOL_basic_ss =
    17.7 -  Simplifier.theory_context @{theory} empty_ss
    17.8 +  Simplifier.theory_context (the_context ()) empty_ss
    17.9      setsubgoaler asm_simp_tac
   17.10      setSSolver safe_solver
   17.11      setSolver unsafe_solver
   17.12 @@ -184,11 +184,11 @@
   17.13    in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
   17.14  
   17.15  val defALL_regroup =
   17.16 -  Simplifier.simproc @{theory}
   17.17 +  Simplifier.simproc (the_context ())
   17.18      "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
   17.19  
   17.20  val defEX_regroup =
   17.21 -  Simplifier.simproc @{theory}
   17.22 +  Simplifier.simproc (the_context ())
   17.23      "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
   17.24  
   17.25  
    18.1 --- a/src/HOLCF/Pcpo.thy	Wed Sep 17 21:27:03 2008 +0200
    18.2 +++ b/src/HOLCF/Pcpo.thy	Wed Sep 17 21:27:08 2008 +0200
    18.3 @@ -209,7 +209,7 @@
    18.4        | _ => SOME meta_UU_reorient;
    18.5  in
    18.6    val UU_reorient_simproc = 
    18.7 -    Simplifier.simproc @{theory} "UU_reorient_simproc" ["UU=x"] reorient_proc
    18.8 +    Simplifier.simproc (the_context ()) "UU_reorient_simproc" ["UU=x"] reorient_proc
    18.9  end;
   18.10  
   18.11  Addsimprocs [UU_reorient_simproc];
    19.1 --- a/src/ZF/Datatype_ZF.thy	Wed Sep 17 21:27:03 2008 +0200
    19.2 +++ b/src/ZF/Datatype_ZF.thy	Wed Sep 17 21:27:08 2008 +0200
    19.3 @@ -103,7 +103,7 @@
    19.4     handle Match => NONE;
    19.5  
    19.6  
    19.7 - val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;
    19.8 + val conv = Simplifier.simproc (the_context ()) "data_free" ["(x::i) = y"] proc;
    19.9  
   19.10  end;
   19.11  
    20.1 --- a/src/ZF/OrdQuant.thy	Wed Sep 17 21:27:03 2008 +0200
    20.2 +++ b/src/ZF/OrdQuant.thy	Wed Sep 17 21:27:08 2008 +0200
    20.3 @@ -382,9 +382,9 @@
    20.4  
    20.5  in
    20.6  
    20.7 -val defREX_regroup = Simplifier.simproc @{theory}
    20.8 +val defREX_regroup = Simplifier.simproc (the_context ())
    20.9    "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
   20.10 -val defRALL_regroup = Simplifier.simproc @{theory}
   20.11 +val defRALL_regroup = Simplifier.simproc (the_context ())
   20.12    "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
   20.13  
   20.14  end;