--- a/src/CCL/CCL.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/CCL/CCL.thy Wed Jul 15 23:50:40 2009 +0200
@@ -1,5 +1,4 @@
(* Title: CCL/CCL.thy
- ID: $Id$
Author: Martin Coen
Copyright 1993 University of Cambridge
*)
@@ -249,13 +248,13 @@
ML {*
-val caseB_lemmas = mk_lemmas (thms "caseBs")
+val caseB_lemmas = mk_lemmas @{thms caseBs}
val ccl_dstncts =
let fun mk_raw_dstnct_thm rls s =
- prove_goal (the_context ()) s (fn _=> [rtac notI 1,eresolve_tac rls 1])
+ prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1])
in map (mk_raw_dstnct_thm caseB_lemmas)
- (mk_dstnct_rls (the_context ()) ["bot","true","false","pair","lambda"]) end
+ (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
fun mk_dstnct_thms thy defs inj_rls xs =
let fun mk_dstnct_thm rls s = prove_goalw thy defs s
@@ -273,9 +272,9 @@
val XH_to_Ds = map XH_to_D
val XH_to_Es = map XH_to_E;
-bind_thms ("ccl_rews", thms "caseBs" @ ccl_injs @ ccl_dstncts);
+bind_thms ("ccl_rews", @{thms caseBs} @ ccl_injs @ ccl_dstncts);
bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [notE]);
-bind_thms ("ccl_injDs", XH_to_Ds (thms "ccl_injs"));
+bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
*}
lemmas [simp] = ccl_rews
@@ -388,13 +387,13 @@
ML {*
local
- fun mk_thm s = prove_goal (the_context ()) s (fn _ =>
- [rtac notI 1,dtac (thm "case_pocong") 1,etac rev_mp 5,
+ fun mk_thm s = prove_goal @{theory} s (fn _ =>
+ [rtac notI 1, dtac @{thm case_pocong} 1, etac rev_mp 5,
ALLGOALS (simp_tac @{simpset}),
- REPEAT (resolve_tac [thm "po_refl", thm "npo_lam_bot"] 1)])
+ REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)])
in
-val npo_rls = [thm "npo_pair_lam", thm "npo_lam_pair"] @ map mk_thm
+val npo_rls = [@{thm npo_pair_lam}, @{thm npo_lam_pair}] @ map mk_thm
["~ true [= false", "~ false [= true",
"~ true [= <a,b>", "~ <a,b> [= true",
"~ true [= lam x. f(x)","~ lam x. f(x) [= true",
--- a/src/CCL/Hered.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/CCL/Hered.thy Wed Jul 15 23:50:40 2009 +0200
@@ -1,5 +1,4 @@
(* Title: CCL/Hered.thy
- ID: $Id$
Author: Martin Coen
Copyright 1993 University of Cambridge
*)
@@ -113,7 +112,7 @@
res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
val HTTgenIs =
- map (mk_genIs (the_context ()) @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
+ map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
["true : HTTgen(R)",
"false : HTTgen(R)",
"[| a : R; b : R |] ==> <a,b> : HTTgen(R)",
--- a/src/CCL/Term.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/CCL/Term.thy Wed Jul 15 23:50:40 2009 +0200
@@ -1,5 +1,4 @@
(* Title: CCL/Term.thy
- ID: $Id$
Author: Martin Coen
Copyright 1993 University of Cambridge
*)
@@ -274,8 +273,9 @@
ML {*
-bind_thms ("term_injs", map (mk_inj_rl (the_context ())
- [thm "applyB", thm "splitB", thm "whenBinl", thm "whenBinr", thm "ncaseBsucc", thm "lcaseBcons"])
+bind_thms ("term_injs", map (mk_inj_rl @{theory}
+ [@{thm applyB}, @{thm splitB}, @{thm whenBinl}, @{thm whenBinr},
+ @{thm ncaseBsucc}, @{thm lcaseBcons}])
["(inl(a) = inl(a')) <-> (a=a')",
"(inr(a) = inr(a')) <-> (a=a')",
"(succ(a) = succ(a')) <-> (a=a')",
@@ -287,7 +287,7 @@
ML {*
bind_thms ("term_dstncts",
- mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs")
+ mkall_dstnct_thms @{theory} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
[["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
*}
@@ -297,8 +297,8 @@
ML {*
local
- fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
- [simp_tac (@{simpset} addsimps (thms "ccl_porews")) 1])
+ fun mk_thm s = prove_goalw @{theory} @{thms data_defs} s (fn _ =>
+ [simp_tac (@{simpset} addsimps @{thms ccl_porews}) 1])
in
val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
"inr(b) [= inr(b') <-> b [= b'",
--- a/src/CCL/Type.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/CCL/Type.thy Wed Jul 15 23:50:40 2009 +0200
@@ -428,7 +428,7 @@
ML {*
-val POgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "POgenXH") (thm "POgen_mono"))
+val POgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm POgenXH} @{thm POgen_mono})
["<true,true> : POgen(R)",
"<false,false> : POgen(R)",
"[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)",
@@ -443,9 +443,9 @@
fun POgen_tac ctxt (rla,rlb) i =
SELECT_GOAL (safe_tac (local_claset_of ctxt)) i THEN
- rtac (rlb RS (rla RS (thm "ssubst_pair"))) i THEN
- (REPEAT (resolve_tac (POgenIs @ [thm "PO_refl" RS (thm "POgen_mono" RS ci3_AI)] @
- (POgenIs RL [thm "POgen_mono" RS ci3_AgenI]) @ [thm "POgen_mono" RS ci3_RI]) i));
+ rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
+ (REPEAT (resolve_tac (POgenIs @ [@{thm PO_refl} RS (@{thm POgen_mono} RS ci3_AI)] @
+ (POgenIs RL [@{thm POgen_mono} RS ci3_AgenI]) @ [@{thm POgen_mono} RS ci3_RI]) i));
*}
@@ -458,7 +458,7 @@
ML {*
-val EQgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "EQgenXH") (thm "EQgen_mono"))
+val EQgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm EQgenXH} @{thm EQgen_mono})
["<true,true> : EQgen(R)",
"<false,false> : EQgen(R)",
"[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
--- a/src/FOL/simpdata.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/FOL/simpdata.ML Wed Jul 15 23:50:40 2009 +0200
@@ -85,11 +85,11 @@
end);
val defEX_regroup =
- Simplifier.simproc (the_context ())
+ Simplifier.simproc @{theory}
"defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
val defALL_regroup =
- Simplifier.simproc (the_context ())
+ Simplifier.simproc @{theory}
"defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
--- a/src/HOL/Algebra/abstract/Ring2.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Wed Jul 15 23:50:40 2009 +0200
@@ -286,7 +286,7 @@
else SOME rew
end;
in
- val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc);
+ val ring_simproc = Simplifier.simproc @{theory} "ring" lhss (K proc);
end;
*}
--- a/src/HOL/Divides.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Divides.thy Wed Jul 15 23:50:40 2009 +0200
@@ -655,7 +655,7 @@
in
-val cancel_div_mod_nat_proc = Simplifier.simproc (the_context ())
+val cancel_div_mod_nat_proc = Simplifier.simproc @{theory}
"cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
val _ = Addsimprocs [cancel_div_mod_nat_proc];
--- a/src/HOL/IntDiv.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/IntDiv.thy Wed Jul 15 23:50:40 2009 +0200
@@ -266,7 +266,7 @@
in
-val cancel_div_mod_int_proc = Simplifier.simproc (the_context ())
+val cancel_div_mod_int_proc = Simplifier.simproc @{theory}
"cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
val _ = Addsimprocs [cancel_div_mod_int_proc];
--- a/src/HOL/Lambda/WeakNorm.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Wed Jul 15 23:50:40 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Lambda/WeakNorm.thy
- ID: $Id$
Author: Stefan Berghofer
Copyright 2003 TU Muenchen
*)
@@ -430,11 +429,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 (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
+val ct1' = cterm_of @{theory} (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 (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
+val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
*}
text {*
@@ -505,11 +504,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 (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
+val ct1' = cterm_of @{theory} (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 (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
+val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
*}
end
--- a/src/HOL/List.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/List.thy Wed Jul 15 23:50:40 2009 +0200
@@ -679,7 +679,7 @@
in
val list_eq_simproc =
- Simplifier.simproc (the_context ()) "list_eq" ["(xs::'a list) = ys"] (K list_eq);
+ Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
end;
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Wed Jul 15 23:50:40 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Modelcheck/EindhovenSyn.thy
- ID: $Id$
Author: Olaf Mueller, Jan Philipps, Robert Sandner
Copyright 1997 TU Muenchen
*)
@@ -70,7 +69,7 @@
val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
val pair_eta_expand_proc =
- Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
+ Simplifier.simproc @{theory} "pair_eta_expand" ["f::'a*'b=>'c"]
(fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
val Eindhoven_ss =
--- a/src/HOL/Modelcheck/MuckeSyn.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Wed Jul 15 23:50:40 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Modelcheck/MuckeSyn.thy
- ID: $Id$
Author: Tobias Hamberger
Copyright 1999 TU Muenchen
*)
@@ -119,7 +118,7 @@
local
- val move_thm = prove_goal (the_context ()) "[| a = b ==> P a; a = b |] ==> P b"
+ val move_thm = prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b"
(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
REPEAT (resolve_tac prems 1)]);
@@ -214,7 +213,7 @@
val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
val pair_eta_expand_proc =
- Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
+ Simplifier.simproc @{theory} "pair_eta_expand" ["f::'a*'b=>'c"]
(fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
val Mucke_ss = @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Jul 15 23:50:40 2009 +0200
@@ -147,7 +147,7 @@
| perm_simproc' thy ss _ = NONE;
val perm_simproc =
- Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
+ Simplifier.simproc @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
val meta_spec = thm "meta_spec";
--- a/src/HOL/Nominal/nominal_permeq.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Wed Jul 15 23:50:40 2009 +0200
@@ -117,7 +117,7 @@
| _ => NONE
end
-val perm_simproc_app = Simplifier.simproc (the_context ()) "perm_simproc_app"
+val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app"
["Nominal.perm pi x"] perm_simproc_app';
(* a simproc that deals with permutation instances in front of functions *)
@@ -137,7 +137,7 @@
| _ => NONE
end
-val perm_simproc_fun = Simplifier.simproc (the_context ()) "perm_simproc_fun"
+val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun"
["Nominal.perm pi x"] perm_simproc_fun';
(* function for simplyfying permutations *)
@@ -217,7 +217,7 @@
end
| _ => NONE);
-val perm_compose_simproc = Simplifier.simproc (the_context ()) "perm_compose"
+val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose"
["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
fun perm_compose_tac ss i =
--- a/src/HOL/OrderedGroup.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/OrderedGroup.thy Wed Jul 15 23:50:40 2009 +0200
@@ -1380,7 +1380,7 @@
if termless_agrp (y, x) then SOME ac2 else NONE
| solve_add_ac thy _ _ = NONE
in
- val add_ac_proc = Simplifier.simproc (the_context ())
+ val add_ac_proc = Simplifier.simproc @{theory}
"add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
end;
--- a/src/HOL/Product_Type.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Product_Type.thy Wed Jul 15 23:50:40 2009 +0200
@@ -470,8 +470,8 @@
| NONE => NONE)
| eta_proc _ _ = NONE;
in
- 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);
+ 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);
end;
Addsimprocs [split_beta_proc, split_eta_proc];
--- a/src/HOL/Prolog/prolog.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML Wed Jul 15 23:50:40 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Prolog/prolog.ML
- ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
@@ -60,7 +59,7 @@
in map zero_var_indexes (at thm) end;
val atomize_ss =
- Simplifier.theory_context (the_context ()) empty_ss
+ Simplifier.theory_context @{theory} empty_ss
setmksimps (mksimps mksimps_pairs)
addsimps [
all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
--- a/src/HOL/Set.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Set.thy Wed Jul 15 23:50:40 2009 +0200
@@ -478,9 +478,9 @@
fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
in
- val defBEX_regroup = Simplifier.simproc (the_context ())
+ val defBEX_regroup = Simplifier.simproc @{theory}
"defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
- val defBALL_regroup = Simplifier.simproc (the_context ())
+ val defBALL_regroup = Simplifier.simproc @{theory}
"defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
end;
@@ -1014,7 +1014,7 @@
ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
in
- val defColl_regroup = Simplifier.simproc (the_context ())
+ val defColl_regroup = Simplifier.simproc @{theory}
"defined Collect" ["{x. P x & Q x}"]
(Quantifier1.rearrange_Coll Coll_perm_tac)
end;
--- a/src/HOL/Statespace/DistinctTreeProver.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Wed Jul 15 23:50:40 2009 +0200
@@ -676,7 +676,7 @@
ML {*
- val ct' = cterm_of (the_context ()) t';
+ val ct' = cterm_of @{theory} t';
*}
ML {*
@@ -706,7 +706,7 @@
ML {*
-val cdist' = cterm_of (the_context ()) dist';
+val cdist' = cterm_of @{theory} dist';
DistinctTreeProver.distinct_implProver (!da) cdist';
*}
--- a/src/HOL/Statespace/state_fun.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Statespace/state_fun.ML Wed Jul 15 23:50:40 2009 +0200
@@ -115,7 +115,7 @@
Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
val lookup_simproc =
- Simplifier.simproc (the_context ()) "lookup_simp" ["lookup d n (update d' c m v s)"]
+ Simplifier.simproc @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
(fn thy => fn ss => fn t =>
(case t of (Const ("StateFun.lookup",lT)$destr$n$
(s as Const ("StateFun.update",uT)$_$_$_$_$_)) =>
@@ -171,7 +171,7 @@
addcongs [thm "block_conj_cong"]);
in
val update_simproc =
- Simplifier.simproc (the_context ()) "update_simp" ["update d c n v s"]
+ Simplifier.simproc @{theory} "update_simp" ["update d c n v s"]
(fn thy => fn ss => fn t =>
(case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
let
--- a/src/HOL/Tools/metis_tools.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Wed Jul 15 23:50:40 2009 +0200
@@ -371,7 +371,7 @@
end;
(* INFERENCE RULE: REFL *)
- val refl_x = cterm_of (the_context ()) (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
+ val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
fun refl_inf ctxt t =
@@ -475,14 +475,14 @@
fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
- 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 equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
+ val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
- 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;
+ 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;
fun type_ext thy tms =
let val subs = ResAtp.tfree_classes_of_terms tms
--- a/src/HOL/Tools/nat_arith.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Tools/nat_arith.ML Wed Jul 15 23:50:40 2009 +0200
@@ -91,18 +91,18 @@
end);
val nat_cancel_sums_add =
- [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
+ [Simplifier.simproc @{theory} "nateq_cancel_sums"
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
(K EqCancelSums.proc),
- Simplifier.simproc (the_context ()) "natless_cancel_sums"
+ Simplifier.simproc @{theory} "natless_cancel_sums"
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
(K LessCancelSums.proc),
- Simplifier.simproc (the_context ()) "natle_cancel_sums"
+ Simplifier.simproc @{theory} "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 (the_context ()) "natdiff_cancel_sums"
+ [Simplifier.simproc @{theory} "natdiff_cancel_sums"
["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
(K DiffCancelSums.proc)];
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Wed Jul 15 23:50:40 2009 +0200
@@ -19,7 +19,7 @@
val numeral_sym_ss = HOL_ss addsimps numeral_syms;
fun rename_numerals th =
- simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
+ simplify numeral_sym_ss (Thm.transfer @{theory} th);
(*Utilities*)
--- a/src/HOL/Tools/numeral.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Tools/numeral.ML Wed Jul 15 23:50:40 2009 +0200
@@ -39,7 +39,7 @@
val oneT = Thm.ctyp_of_term one;
val number_of = @{cpat "number_of"};
-val numberT = Thm.ctyp_of (the_context ()) (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
+val numberT = Thm.ctyp_of @{theory} (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 Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Wed Jul 15 23:50:40 2009 +0200
@@ -154,9 +154,9 @@
val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
-val [f_B,g_B] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_B}));
-val [g_C,f_C] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_C}));
-val [f_S,g_S] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_S}));
+val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
+val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
+val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.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 Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Wed Jul 15 23:50:40 2009 +0200
@@ -15,8 +15,8 @@
open Proofterm;
-val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) true) o
- Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
+val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o
+ Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
(** eliminate meta-equality rules **)
--- a/src/HOL/Tools/sat_funcs.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Wed Jul 15 23:50:40 2009 +0200
@@ -66,16 +66,10 @@
val counter = ref 0;
-val resolution_thm = (* "[| ?P ==> False; ~ ?P ==> False |] ==> False" *)
- let
- val cterm = cterm_of (the_context ())
- val Q = Var (("Q", 0), HOLogic.boolT)
- val False = HOLogic.false_const
- in
- Thm.instantiate ([], [(cterm Q, cterm False)]) @{thm case_split}
- end;
+val resolution_thm =
+ @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
-val cP = cterm_of (theory_of_thm resolution_thm) (Var (("P", 0), HOLogic.boolT));
+val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
(* ------------------------------------------------------------------------- *)
(* lit_ord: an order on integers that considers their absolute values only, *)
--- a/src/HOL/Tools/simpdata.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOL/Tools/simpdata.ML Wed Jul 15 23:50:40 2009 +0200
@@ -181,11 +181,11 @@
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
val defALL_regroup =
- Simplifier.simproc (the_context ())
+ Simplifier.simproc @{theory}
"defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
val defEX_regroup =
- Simplifier.simproc (the_context ())
+ Simplifier.simproc @{theory}
"defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
--- a/src/HOLCF/holcf_logic.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/HOLCF/holcf_logic.ML Wed Jul 15 23:50:40 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOLCF/holcf_logic.ML
- ID: $Id$
Author: David von Oheimb
Abstract syntax operations for HOLCF.
@@ -10,7 +9,6 @@
signature HOLCF_LOGIC =
sig
val mk_btyp: string -> typ * typ -> typ
- val pcpoC: class
val pcpoS: sort
val mk_TFree: string -> typ
val cfun_arrow: string
@@ -27,8 +25,7 @@
(* sort pcpo *)
-val pcpoC = Sign.intern_class (the_context ()) "pcpo";
-val pcpoS = [pcpoC];
+val pcpoS = @{sort pcpo};
fun mk_TFree s = TFree ("'" ^ s, pcpoS);
--- a/src/Pure/Isar/theory_target.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML Wed Jul 15 23:50:40 2009 +0200
@@ -177,7 +177,6 @@
let
val b' = Morphism.binding phi b;
val rhs' = Morphism.term phi rhs;
- val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
val arg = (b', Term.close_schematic_term rhs');
val similar_body = Type.similar_types (rhs, rhs');
(* FIXME workaround based on educated guess *)
@@ -188,7 +187,7 @@
in
not (is_class andalso (similar_body orelse class_global)) ?
(Context.mapping_result
- (Sign.add_abbrev PrintMode.internal tags legacy_arg)
+ (Sign.add_abbrev PrintMode.internal tags arg)
(ProofContext.add_abbrev PrintMode.internal tags arg)
#-> (fn (lhs' as Const (d, _), _) =>
similar_body ?
--- a/src/Pure/logic.ML Wed Jul 15 22:30:27 2009 +0200
+++ b/src/Pure/logic.ML Wed Jul 15 23:50:40 2009 +0200
@@ -424,6 +424,8 @@
a $ Abs(c, T, list_rename_params (cs, t))
| list_rename_params (cs, B) = B;
+
+
(*** Treatment of "assume", "erule", etc. ***)
(*Strips assumptions in goal yielding
@@ -440,8 +442,7 @@
strip_assums_imp (nasms-1, H::Hs, B)
| strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
-
-(*Strips OUTER parameters only, unlike similar legacy versions.*)
+(*Strips OUTER parameters only.*)
fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
strip_assums_all ((a,T)::params, t)
| strip_assums_all (params, B) = (params, B);
--- a/src/ZF/Datatype_ZF.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/ZF/Datatype_ZF.thy Wed Jul 15 23:50:40 2009 +0200
@@ -1,8 +1,6 @@
(* Title: ZF/Datatype.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
-
*)
header{*Datatype and CoDatatype Definitions*}
@@ -103,7 +101,7 @@
handle Match => NONE;
- val conv = Simplifier.simproc (the_context ()) "data_free" ["(x::i) = y"] proc;
+ val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;
end;
--- a/src/ZF/OrdQuant.thy Wed Jul 15 22:30:27 2009 +0200
+++ b/src/ZF/OrdQuant.thy Wed Jul 15 23:50:40 2009 +0200
@@ -1,5 +1,4 @@
(* Title: ZF/AC/OrdQuant.thy
- ID: $Id$
Authors: Krzysztof Grabczewski and L C Paulson
*)
@@ -382,9 +381,9 @@
in
-val defREX_regroup = Simplifier.simproc (the_context ())
+val defREX_regroup = Simplifier.simproc @{theory}
"defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
-val defRALL_regroup = Simplifier.simproc (the_context ())
+val defRALL_regroup = Simplifier.simproc @{theory}
"defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
end;