more antiquotations;
authorwenzelm
Wed Jul 15 23:48:21 2009 +0200 (2009-07-15)
changeset 32010cb1a1c94b4cd
parent 32009 fd3c60ad9155
child 32012 f2a8dbceb615
more antiquotations;
src/CCL/CCL.thy
src/CCL/Hered.thy
src/CCL/Term.thy
src/CCL/Type.thy
src/FOL/simpdata.ML
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Divides.thy
src/HOL/IntDiv.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/List.thy
src/HOL/Modelcheck/EindhovenSyn.thy
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/OrderedGroup.thy
src/HOL/Product_Type.thy
src/HOL/Prolog/prolog.ML
src/HOL/Set.thy
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/nat_arith.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/rewrite_hol_proof.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/simpdata.ML
src/HOLCF/holcf_logic.ML
src/ZF/Datatype_ZF.thy
src/ZF/OrdQuant.thy
     1.1 --- a/src/CCL/CCL.thy	Wed Jul 15 23:11:57 2009 +0200
     1.2 +++ b/src/CCL/CCL.thy	Wed Jul 15 23:48:21 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      CCL/CCL.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Martin Coen
     1.7      Copyright   1993  University of Cambridge
     1.8  *)
     1.9 @@ -249,13 +248,13 @@
    1.10  
    1.11  ML {*
    1.12  
    1.13 -val caseB_lemmas = mk_lemmas (thms "caseBs")
    1.14 +val caseB_lemmas = mk_lemmas @{thms caseBs}
    1.15  
    1.16  val ccl_dstncts =
    1.17          let fun mk_raw_dstnct_thm rls s =
    1.18 -                  prove_goal (the_context ()) s (fn _=> [rtac notI 1,eresolve_tac rls 1])
    1.19 +                  prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1])
    1.20          in map (mk_raw_dstnct_thm caseB_lemmas)
    1.21 -                (mk_dstnct_rls (the_context ()) ["bot","true","false","pair","lambda"]) end
    1.22 +                (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
    1.23  
    1.24  fun mk_dstnct_thms thy defs inj_rls xs =
    1.25            let fun mk_dstnct_thm rls s = prove_goalw thy defs s
    1.26 @@ -273,9 +272,9 @@
    1.27  val XH_to_Ds = map XH_to_D
    1.28  val XH_to_Es = map XH_to_E;
    1.29  
    1.30 -bind_thms ("ccl_rews", thms "caseBs" @ ccl_injs @ ccl_dstncts);
    1.31 +bind_thms ("ccl_rews", @{thms caseBs} @ ccl_injs @ ccl_dstncts);
    1.32  bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [notE]);
    1.33 -bind_thms ("ccl_injDs", XH_to_Ds (thms "ccl_injs"));
    1.34 +bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
    1.35  *}
    1.36  
    1.37  lemmas [simp] = ccl_rews
    1.38 @@ -388,13 +387,13 @@
    1.39  ML {*
    1.40  
    1.41  local
    1.42 -  fun mk_thm s = prove_goal (the_context ()) s (fn _ =>
    1.43 -                          [rtac notI 1,dtac (thm "case_pocong") 1,etac rev_mp 5,
    1.44 +  fun mk_thm s = prove_goal @{theory} s (fn _ =>
    1.45 +                          [rtac notI 1, dtac @{thm case_pocong} 1, etac rev_mp 5,
    1.46                             ALLGOALS (simp_tac @{simpset}),
    1.47 -                           REPEAT (resolve_tac [thm "po_refl", thm "npo_lam_bot"] 1)])
    1.48 +                           REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)])
    1.49  in
    1.50  
    1.51 -val npo_rls = [thm "npo_pair_lam", thm "npo_lam_pair"] @ map mk_thm
    1.52 +val npo_rls = [@{thm npo_pair_lam}, @{thm npo_lam_pair}] @ map mk_thm
    1.53              ["~ true [= false",          "~ false [= true",
    1.54               "~ true [= <a,b>",          "~ <a,b> [= true",
    1.55               "~ true [= lam x. f(x)","~ lam x. f(x) [= true",
     2.1 --- a/src/CCL/Hered.thy	Wed Jul 15 23:11:57 2009 +0200
     2.2 +++ b/src/CCL/Hered.thy	Wed Jul 15 23:48:21 2009 +0200
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      CCL/Hered.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Martin Coen
     2.7      Copyright   1993  University of Cambridge
     2.8  *)
     2.9 @@ -113,7 +112,7 @@
    2.10    res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
    2.11  
    2.12  val HTTgenIs =
    2.13 -  map (mk_genIs (the_context ()) @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
    2.14 +  map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
    2.15    ["true : HTTgen(R)",
    2.16     "false : HTTgen(R)",
    2.17     "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
     3.1 --- a/src/CCL/Term.thy	Wed Jul 15 23:11:57 2009 +0200
     3.2 +++ b/src/CCL/Term.thy	Wed Jul 15 23:48:21 2009 +0200
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      CCL/Term.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Martin Coen
     3.7      Copyright   1993  University of Cambridge
     3.8  *)
     3.9 @@ -274,8 +273,9 @@
    3.10  
    3.11  ML {*
    3.12  
    3.13 -bind_thms ("term_injs", map (mk_inj_rl (the_context ())
    3.14 -  [thm "applyB", thm "splitB", thm "whenBinl", thm "whenBinr", thm "ncaseBsucc", thm "lcaseBcons"])
    3.15 +bind_thms ("term_injs", map (mk_inj_rl @{theory}
    3.16 +  [@{thm applyB}, @{thm splitB}, @{thm whenBinl}, @{thm whenBinr},
    3.17 +    @{thm ncaseBsucc}, @{thm lcaseBcons}])
    3.18      ["(inl(a) = inl(a')) <-> (a=a')",
    3.19       "(inr(a) = inr(a')) <-> (a=a')",
    3.20       "(succ(a) = succ(a')) <-> (a=a')",
    3.21 @@ -287,7 +287,7 @@
    3.22  
    3.23  ML {*
    3.24  bind_thms ("term_dstncts",
    3.25 -  mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs")
    3.26 +  mkall_dstnct_thms @{theory} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
    3.27      [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
    3.28  *}
    3.29  
    3.30 @@ -297,8 +297,8 @@
    3.31  ML {*
    3.32  
    3.33  local
    3.34 -  fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
    3.35 -    [simp_tac (@{simpset} addsimps (thms "ccl_porews")) 1])
    3.36 +  fun mk_thm s = prove_goalw @{theory} @{thms data_defs} s (fn _ =>
    3.37 +    [simp_tac (@{simpset} addsimps @{thms ccl_porews}) 1])
    3.38  in
    3.39    val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
    3.40                                  "inr(b) [= inr(b') <-> b [= b'",
     4.1 --- a/src/CCL/Type.thy	Wed Jul 15 23:11:57 2009 +0200
     4.2 +++ b/src/CCL/Type.thy	Wed Jul 15 23:48:21 2009 +0200
     4.3 @@ -428,7 +428,7 @@
     4.4  
     4.5  ML {*
     4.6  
     4.7 -val POgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "POgenXH") (thm "POgen_mono"))
     4.8 +val POgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm POgenXH} @{thm POgen_mono})
     4.9    ["<true,true> : POgen(R)",
    4.10     "<false,false> : POgen(R)",
    4.11     "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)",
    4.12 @@ -443,9 +443,9 @@
    4.13  
    4.14  fun POgen_tac ctxt (rla,rlb) i =
    4.15    SELECT_GOAL (safe_tac (local_claset_of ctxt)) i THEN
    4.16 -  rtac (rlb RS (rla RS (thm "ssubst_pair"))) i THEN
    4.17 -  (REPEAT (resolve_tac (POgenIs @ [thm "PO_refl" RS (thm "POgen_mono" RS ci3_AI)] @
    4.18 -    (POgenIs RL [thm "POgen_mono" RS ci3_AgenI]) @ [thm "POgen_mono" RS ci3_RI]) i));
    4.19 +  rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
    4.20 +  (REPEAT (resolve_tac (POgenIs @ [@{thm PO_refl} RS (@{thm POgen_mono} RS ci3_AI)] @
    4.21 +    (POgenIs RL [@{thm POgen_mono} RS ci3_AgenI]) @ [@{thm POgen_mono} RS ci3_RI]) i));
    4.22  
    4.23  *}
    4.24  
    4.25 @@ -458,7 +458,7 @@
    4.26  
    4.27  ML {*
    4.28  
    4.29 -val EQgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "EQgenXH") (thm "EQgen_mono"))
    4.30 +val EQgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm EQgenXH} @{thm EQgen_mono})
    4.31    ["<true,true> : EQgen(R)",
    4.32     "<false,false> : EQgen(R)",
    4.33     "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
     5.1 --- a/src/FOL/simpdata.ML	Wed Jul 15 23:11:57 2009 +0200
     5.2 +++ b/src/FOL/simpdata.ML	Wed Jul 15 23:48:21 2009 +0200
     5.3 @@ -85,11 +85,11 @@
     5.4  end);
     5.5  
     5.6  val defEX_regroup =
     5.7 -  Simplifier.simproc (the_context ())
     5.8 +  Simplifier.simproc @{theory}
     5.9      "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
    5.10  
    5.11  val defALL_regroup =
    5.12 -  Simplifier.simproc (the_context ())
    5.13 +  Simplifier.simproc @{theory}
    5.14      "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
    5.15  
    5.16  
     6.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Jul 15 23:11:57 2009 +0200
     6.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Jul 15 23:48:21 2009 +0200
     6.3 @@ -286,7 +286,7 @@
     6.4          else SOME rew 
     6.5      end;
     6.6    in
     6.7 -    val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc);
     6.8 +    val ring_simproc = Simplifier.simproc @{theory} "ring" lhss (K proc);
     6.9    end;
    6.10  *}
    6.11  
     7.1 --- a/src/HOL/Divides.thy	Wed Jul 15 23:11:57 2009 +0200
     7.2 +++ b/src/HOL/Divides.thy	Wed Jul 15 23:48:21 2009 +0200
     7.3 @@ -655,7 +655,7 @@
     7.4  
     7.5  in
     7.6  
     7.7 -val cancel_div_mod_nat_proc = Simplifier.simproc (the_context ())
     7.8 +val cancel_div_mod_nat_proc = Simplifier.simproc @{theory}
     7.9    "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
    7.10  
    7.11  val _ = Addsimprocs [cancel_div_mod_nat_proc];
     8.1 --- a/src/HOL/IntDiv.thy	Wed Jul 15 23:11:57 2009 +0200
     8.2 +++ b/src/HOL/IntDiv.thy	Wed Jul 15 23:48:21 2009 +0200
     8.3 @@ -266,7 +266,7 @@
     8.4  
     8.5  in
     8.6  
     8.7 -val cancel_div_mod_int_proc = Simplifier.simproc (the_context ())
     8.8 +val cancel_div_mod_int_proc = Simplifier.simproc @{theory}
     8.9    "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
    8.10  
    8.11  val _ = Addsimprocs [cancel_div_mod_int_proc];
     9.1 --- a/src/HOL/Lambda/WeakNorm.thy	Wed Jul 15 23:11:57 2009 +0200
     9.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Wed Jul 15 23:48:21 2009 +0200
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      HOL/Lambda/WeakNorm.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Stefan Berghofer
     9.7      Copyright   2003 TU Muenchen
     9.8  *)
     9.9 @@ -430,11 +429,11 @@
    9.10  
    9.11  val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
    9.12  val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1));
    9.13 -val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
    9.14 +val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
    9.15  
    9.16  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)))))"};
    9.17  val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
    9.18 -val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
    9.19 +val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
    9.20  *}
    9.21  
    9.22  text {*
    9.23 @@ -505,11 +504,11 @@
    9.24  ML {*
    9.25  val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
    9.26  val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
    9.27 -val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
    9.28 +val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
    9.29  
    9.30  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)))))"};
    9.31  val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
    9.32 -val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
    9.33 +val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
    9.34  *}
    9.35  
    9.36  end
    10.1 --- a/src/HOL/List.thy	Wed Jul 15 23:11:57 2009 +0200
    10.2 +++ b/src/HOL/List.thy	Wed Jul 15 23:48:21 2009 +0200
    10.3 @@ -679,7 +679,7 @@
    10.4  in
    10.5  
    10.6  val list_eq_simproc =
    10.7 -  Simplifier.simproc (the_context ()) "list_eq" ["(xs::'a list) = ys"] (K list_eq);
    10.8 +  Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
    10.9  
   10.10  end;
   10.11  
    11.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Jul 15 23:11:57 2009 +0200
    11.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Jul 15 23:48:21 2009 +0200
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      HOL/Modelcheck/EindhovenSyn.thy
    11.5 -    ID:         $Id$
    11.6      Author:     Olaf Mueller, Jan Philipps, Robert Sandner
    11.7      Copyright   1997  TU Muenchen
    11.8  *)
    11.9 @@ -70,7 +69,7 @@
   11.10  val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
   11.11  
   11.12  val pair_eta_expand_proc =
   11.13 -  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
   11.14 +  Simplifier.simproc @{theory} "pair_eta_expand" ["f::'a*'b=>'c"]
   11.15    (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
   11.16  
   11.17  val Eindhoven_ss =
    12.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Wed Jul 15 23:11:57 2009 +0200
    12.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Wed Jul 15 23:48:21 2009 +0200
    12.3 @@ -1,5 +1,4 @@
    12.4  (*  Title:      HOL/Modelcheck/MuckeSyn.thy
    12.5 -    ID:         $Id$
    12.6      Author:     Tobias Hamberger
    12.7      Copyright   1999  TU Muenchen
    12.8  *)
    12.9 @@ -119,7 +118,7 @@
   12.10  
   12.11  local
   12.12  
   12.13 -  val move_thm = prove_goal (the_context ()) "[| a = b ==> P a; a = b |] ==> P b"
   12.14 +  val move_thm = prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b"
   12.15  	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
   12.16  		     REPEAT (resolve_tac prems 1)]);
   12.17  
   12.18 @@ -214,7 +213,7 @@
   12.19  val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
   12.20  
   12.21  val pair_eta_expand_proc =
   12.22 -  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
   12.23 +  Simplifier.simproc @{theory} "pair_eta_expand" ["f::'a*'b=>'c"]
   12.24    (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
   12.25  
   12.26  val Mucke_ss = @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
    13.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 15 23:11:57 2009 +0200
    13.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 15 23:48:21 2009 +0200
    13.3 @@ -147,7 +147,7 @@
    13.4    | perm_simproc' thy ss _ = NONE;
    13.5  
    13.6  val perm_simproc =
    13.7 -  Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
    13.8 +  Simplifier.simproc @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
    13.9  
   13.10  val meta_spec = thm "meta_spec";
   13.11  
    14.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Jul 15 23:11:57 2009 +0200
    14.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Jul 15 23:48:21 2009 +0200
    14.3 @@ -117,7 +117,7 @@
    14.4        | _ => NONE
    14.5    end
    14.6  
    14.7 -val perm_simproc_app = Simplifier.simproc (the_context ()) "perm_simproc_app"
    14.8 +val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app"
    14.9    ["Nominal.perm pi x"] perm_simproc_app';
   14.10  
   14.11  (* a simproc that deals with permutation instances in front of functions  *)
   14.12 @@ -137,7 +137,7 @@
   14.13        | _ => NONE
   14.14     end
   14.15  
   14.16 -val perm_simproc_fun = Simplifier.simproc (the_context ()) "perm_simproc_fun"
   14.17 +val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun"
   14.18    ["Nominal.perm pi x"] perm_simproc_fun';
   14.19  
   14.20  (* function for simplyfying permutations          *)
   14.21 @@ -217,7 +217,7 @@
   14.22      end
   14.23    | _ => NONE);
   14.24  
   14.25 -val perm_compose_simproc = Simplifier.simproc (the_context ()) "perm_compose"
   14.26 +val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose"
   14.27    ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
   14.28  
   14.29  fun perm_compose_tac ss i = 
    15.1 --- a/src/HOL/OrderedGroup.thy	Wed Jul 15 23:11:57 2009 +0200
    15.2 +++ b/src/HOL/OrderedGroup.thy	Wed Jul 15 23:48:21 2009 +0200
    15.3 @@ -1380,7 +1380,7 @@
    15.4          if termless_agrp (y, x) then SOME ac2 else NONE
    15.5      | solve_add_ac thy _ _ = NONE
    15.6  in
    15.7 -  val add_ac_proc = Simplifier.simproc (the_context ())
    15.8 +  val add_ac_proc = Simplifier.simproc @{theory}
    15.9      "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
   15.10  end;
   15.11  
    16.1 --- a/src/HOL/Product_Type.thy	Wed Jul 15 23:11:57 2009 +0200
    16.2 +++ b/src/HOL/Product_Type.thy	Wed Jul 15 23:48:21 2009 +0200
    16.3 @@ -470,8 +470,8 @@
    16.4          | NONE => NONE)
    16.5    |   eta_proc _ _ = NONE;
    16.6  in
    16.7 -  val split_beta_proc = Simplifier.simproc (the_context ()) "split_beta" ["split f z"] (K beta_proc);
    16.8 -  val split_eta_proc = Simplifier.simproc (the_context ()) "split_eta" ["split f"] (K eta_proc);
    16.9 +  val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
   16.10 +  val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
   16.11  end;
   16.12  
   16.13  Addsimprocs [split_beta_proc, split_eta_proc];
    17.1 --- a/src/HOL/Prolog/prolog.ML	Wed Jul 15 23:11:57 2009 +0200
    17.2 +++ b/src/HOL/Prolog/prolog.ML	Wed Jul 15 23:48:21 2009 +0200
    17.3 @@ -1,5 +1,4 @@
    17.4  (*  Title:    HOL/Prolog/prolog.ML
    17.5 -    ID:       $Id$
    17.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
    17.7  *)
    17.8  
    17.9 @@ -60,7 +59,7 @@
   17.10  in map zero_var_indexes (at thm) end;
   17.11  
   17.12  val atomize_ss =
   17.13 -  Simplifier.theory_context (the_context ()) empty_ss
   17.14 +  Simplifier.theory_context @{theory} empty_ss
   17.15    setmksimps (mksimps mksimps_pairs)
   17.16    addsimps [
   17.17          all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    18.1 --- a/src/HOL/Set.thy	Wed Jul 15 23:11:57 2009 +0200
    18.2 +++ b/src/HOL/Set.thy	Wed Jul 15 23:48:21 2009 +0200
    18.3 @@ -478,9 +478,9 @@
    18.4      fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    18.5      val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    18.6    in
    18.7 -    val defBEX_regroup = Simplifier.simproc (the_context ())
    18.8 +    val defBEX_regroup = Simplifier.simproc @{theory}
    18.9        "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
   18.10 -    val defBALL_regroup = Simplifier.simproc (the_context ())
   18.11 +    val defBALL_regroup = Simplifier.simproc @{theory}
   18.12        "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
   18.13    end;
   18.14  
   18.15 @@ -1014,7 +1014,7 @@
   18.16      ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
   18.17                      DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
   18.18    in
   18.19 -    val defColl_regroup = Simplifier.simproc (the_context ())
   18.20 +    val defColl_regroup = Simplifier.simproc @{theory}
   18.21        "defined Collect" ["{x. P x & Q x}"]
   18.22        (Quantifier1.rearrange_Coll Coll_perm_tac)
   18.23    end;
    19.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Wed Jul 15 23:11:57 2009 +0200
    19.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Wed Jul 15 23:48:21 2009 +0200
    19.3 @@ -676,7 +676,7 @@
    19.4  
    19.5  
    19.6  ML {* 
    19.7 - val ct' = cterm_of (the_context ()) t';
    19.8 + val ct' = cterm_of @{theory} t';
    19.9  *}
   19.10  
   19.11  ML {*
   19.12 @@ -706,7 +706,7 @@
   19.13  
   19.14  
   19.15  ML {*
   19.16 -val cdist' = cterm_of (the_context ()) dist';
   19.17 +val cdist' = cterm_of @{theory} dist';
   19.18  DistinctTreeProver.distinct_implProver (!da) cdist';
   19.19  *}
   19.20  
    20.1 --- a/src/HOL/Statespace/state_fun.ML	Wed Jul 15 23:11:57 2009 +0200
    20.2 +++ b/src/HOL/Statespace/state_fun.ML	Wed Jul 15 23:48:21 2009 +0200
    20.3 @@ -115,7 +115,7 @@
    20.4    Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
    20.5  
    20.6  val lookup_simproc =
    20.7 -  Simplifier.simproc (the_context ()) "lookup_simp" ["lookup d n (update d' c m v s)"]
    20.8 +  Simplifier.simproc @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
    20.9      (fn thy => fn ss => fn t =>
   20.10        (case t of (Const ("StateFun.lookup",lT)$destr$n$
   20.11                     (s as Const ("StateFun.update",uT)$_$_$_$_$_)) =>
   20.12 @@ -171,7 +171,7 @@
   20.13                   addcongs [thm "block_conj_cong"]);
   20.14  in
   20.15  val update_simproc =
   20.16 -  Simplifier.simproc (the_context ()) "update_simp" ["update d c n v s"]
   20.17 +  Simplifier.simproc @{theory} "update_simp" ["update d c n v s"]
   20.18      (fn thy => fn ss => fn t =>
   20.19        (case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
   20.20           let 
    21.1 --- a/src/HOL/Tools/metis_tools.ML	Wed Jul 15 23:11:57 2009 +0200
    21.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Jul 15 23:48:21 2009 +0200
    21.3 @@ -371,7 +371,7 @@
    21.4      end;
    21.5  
    21.6    (* INFERENCE RULE: REFL *)
    21.7 -  val refl_x = cterm_of (the_context ()) (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
    21.8 +  val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
    21.9    val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   21.10  
   21.11    fun refl_inf ctxt t =
   21.12 @@ -475,14 +475,14 @@
   21.13  
   21.14    fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
   21.15  
   21.16 -  val equal_imp_fequal' = cnf_th (the_context ()) (thm"equal_imp_fequal");
   21.17 -  val fequal_imp_equal' = cnf_th (the_context ()) (thm"fequal_imp_equal");
   21.18 +  val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
   21.19 +  val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
   21.20  
   21.21 -  val comb_I = cnf_th (the_context ()) ResHolClause.comb_I;
   21.22 -  val comb_K = cnf_th (the_context ()) ResHolClause.comb_K;
   21.23 -  val comb_B = cnf_th (the_context ()) ResHolClause.comb_B;
   21.24 -  val comb_C = cnf_th (the_context ()) ResHolClause.comb_C;
   21.25 -  val comb_S = cnf_th (the_context ()) ResHolClause.comb_S;
   21.26 +  val comb_I = cnf_th @{theory} ResHolClause.comb_I;
   21.27 +  val comb_K = cnf_th @{theory} ResHolClause.comb_K;
   21.28 +  val comb_B = cnf_th @{theory} ResHolClause.comb_B;
   21.29 +  val comb_C = cnf_th @{theory} ResHolClause.comb_C;
   21.30 +  val comb_S = cnf_th @{theory} ResHolClause.comb_S;
   21.31  
   21.32    fun type_ext thy tms =
   21.33      let val subs = ResAtp.tfree_classes_of_terms tms
    22.1 --- a/src/HOL/Tools/nat_arith.ML	Wed Jul 15 23:11:57 2009 +0200
    22.2 +++ b/src/HOL/Tools/nat_arith.ML	Wed Jul 15 23:48:21 2009 +0200
    22.3 @@ -91,18 +91,18 @@
    22.4  end);
    22.5  
    22.6  val nat_cancel_sums_add =
    22.7 -  [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
    22.8 +  [Simplifier.simproc @{theory} "nateq_cancel_sums"
    22.9       ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
   22.10       (K EqCancelSums.proc),
   22.11 -   Simplifier.simproc (the_context ()) "natless_cancel_sums"
   22.12 +   Simplifier.simproc @{theory} "natless_cancel_sums"
   22.13       ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
   22.14       (K LessCancelSums.proc),
   22.15 -   Simplifier.simproc (the_context ()) "natle_cancel_sums"
   22.16 +   Simplifier.simproc @{theory} "natle_cancel_sums"
   22.17       ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
   22.18       (K LeCancelSums.proc)];
   22.19  
   22.20  val nat_cancel_sums = nat_cancel_sums_add @
   22.21 -  [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
   22.22 +  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
   22.23      ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
   22.24      (K DiffCancelSums.proc)];
   22.25  
    23.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Jul 15 23:11:57 2009 +0200
    23.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Jul 15 23:48:21 2009 +0200
    23.3 @@ -19,7 +19,7 @@
    23.4  val numeral_sym_ss = HOL_ss addsimps numeral_syms;
    23.5  
    23.6  fun rename_numerals th =
    23.7 -    simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
    23.8 +    simplify numeral_sym_ss (Thm.transfer @{theory} th);
    23.9  
   23.10  (*Utilities*)
   23.11  
    24.1 --- a/src/HOL/Tools/numeral.ML	Wed Jul 15 23:11:57 2009 +0200
    24.2 +++ b/src/HOL/Tools/numeral.ML	Wed Jul 15 23:48:21 2009 +0200
    24.3 @@ -39,7 +39,7 @@
    24.4  val oneT = Thm.ctyp_of_term one;
    24.5  
    24.6  val number_of = @{cpat "number_of"};
    24.7 -val numberT = Thm.ctyp_of (the_context ()) (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
    24.8 +val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
    24.9  
   24.10  fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
   24.11  
    25.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Jul 15 23:11:57 2009 +0200
    25.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Jul 15 23:48:21 2009 +0200
    25.3 @@ -154,9 +154,9 @@
    25.4  
    25.5  val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
    25.6  
    25.7 -val [f_B,g_B] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_B}));
    25.8 -val [g_C,f_C] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_C}));
    25.9 -val [f_S,g_S] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_S}));
   25.10 +val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
   25.11 +val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
   25.12 +val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
   25.13  
   25.14  (*FIXME: requires more use of cterm constructors*)
   25.15  fun abstract ct =
    26.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Wed Jul 15 23:11:57 2009 +0200
    26.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Wed Jul 15 23:48:21 2009 +0200
    26.3 @@ -15,8 +15,8 @@
    26.4  
    26.5  open Proofterm;
    26.6  
    26.7 -val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) true) o
    26.8 -    Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
    26.9 +val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o
   26.10 +    Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
   26.11  
   26.12    (** eliminate meta-equality rules **)
   26.13  
    27.1 --- a/src/HOL/Tools/sat_funcs.ML	Wed Jul 15 23:11:57 2009 +0200
    27.2 +++ b/src/HOL/Tools/sat_funcs.ML	Wed Jul 15 23:48:21 2009 +0200
    27.3 @@ -66,16 +66,10 @@
    27.4  
    27.5  val counter = ref 0;
    27.6  
    27.7 -val resolution_thm =  (* "[| ?P ==> False; ~ ?P ==> False |] ==> False" *)
    27.8 -	let
    27.9 -		val cterm = cterm_of (the_context ())
   27.10 -		val Q     = Var (("Q", 0), HOLogic.boolT)
   27.11 -		val False = HOLogic.false_const
   27.12 -	in
   27.13 -		Thm.instantiate ([], [(cterm Q, cterm False)]) @{thm case_split}
   27.14 -	end;
   27.15 +val resolution_thm =
   27.16 +  @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
   27.17  
   27.18 -val cP = cterm_of (theory_of_thm resolution_thm) (Var (("P", 0), HOLogic.boolT));
   27.19 +val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
   27.20  
   27.21  (* ------------------------------------------------------------------------- *)
   27.22  (* lit_ord: an order on integers that considers their absolute values only,  *)
    28.1 --- a/src/HOL/Tools/simpdata.ML	Wed Jul 15 23:11:57 2009 +0200
    28.2 +++ b/src/HOL/Tools/simpdata.ML	Wed Jul 15 23:48:21 2009 +0200
    28.3 @@ -181,11 +181,11 @@
    28.4    in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
    28.5  
    28.6  val defALL_regroup =
    28.7 -  Simplifier.simproc (the_context ())
    28.8 +  Simplifier.simproc @{theory}
    28.9      "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
   28.10  
   28.11  val defEX_regroup =
   28.12 -  Simplifier.simproc (the_context ())
   28.13 +  Simplifier.simproc @{theory}
   28.14      "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
   28.15  
   28.16  
    29.1 --- a/src/HOLCF/holcf_logic.ML	Wed Jul 15 23:11:57 2009 +0200
    29.2 +++ b/src/HOLCF/holcf_logic.ML	Wed Jul 15 23:48:21 2009 +0200
    29.3 @@ -1,5 +1,4 @@
    29.4  (*  Title:      HOLCF/holcf_logic.ML
    29.5 -    ID:         $Id$
    29.6      Author:     David von Oheimb
    29.7  
    29.8  Abstract syntax operations for HOLCF.
    29.9 @@ -10,7 +9,6 @@
   29.10  signature HOLCF_LOGIC =
   29.11  sig
   29.12    val mk_btyp: string -> typ * typ -> typ
   29.13 -  val pcpoC: class
   29.14    val pcpoS: sort
   29.15    val mk_TFree: string -> typ
   29.16    val cfun_arrow: string
   29.17 @@ -27,8 +25,7 @@
   29.18  
   29.19  (* sort pcpo *)
   29.20  
   29.21 -val pcpoC = Sign.intern_class (the_context ()) "pcpo";
   29.22 -val pcpoS = [pcpoC];
   29.23 +val pcpoS = @{sort pcpo};
   29.24  fun mk_TFree s = TFree ("'" ^ s, pcpoS);
   29.25  
   29.26  
    30.1 --- a/src/ZF/Datatype_ZF.thy	Wed Jul 15 23:11:57 2009 +0200
    30.2 +++ b/src/ZF/Datatype_ZF.thy	Wed Jul 15 23:48:21 2009 +0200
    30.3 @@ -1,8 +1,6 @@
    30.4  (*  Title:      ZF/Datatype.thy
    30.5 -    ID:         $Id$
    30.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    30.7      Copyright   1997  University of Cambridge
    30.8 -
    30.9  *)
   30.10  
   30.11  header{*Datatype and CoDatatype Definitions*}
   30.12 @@ -103,7 +101,7 @@
   30.13     handle Match => NONE;
   30.14  
   30.15  
   30.16 - val conv = Simplifier.simproc (the_context ()) "data_free" ["(x::i) = y"] proc;
   30.17 + val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;
   30.18  
   30.19  end;
   30.20  
    31.1 --- a/src/ZF/OrdQuant.thy	Wed Jul 15 23:11:57 2009 +0200
    31.2 +++ b/src/ZF/OrdQuant.thy	Wed Jul 15 23:48:21 2009 +0200
    31.3 @@ -1,5 +1,4 @@
    31.4  (*  Title:      ZF/AC/OrdQuant.thy
    31.5 -    ID:         $Id$
    31.6      Authors:    Krzysztof Grabczewski and L C Paulson
    31.7  *)
    31.8  
    31.9 @@ -382,9 +381,9 @@
   31.10  
   31.11  in
   31.12  
   31.13 -val defREX_regroup = Simplifier.simproc (the_context ())
   31.14 +val defREX_regroup = Simplifier.simproc @{theory}
   31.15    "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
   31.16 -val defRALL_regroup = Simplifier.simproc (the_context ())
   31.17 +val defRALL_regroup = Simplifier.simproc @{theory}
   31.18    "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
   31.19  
   31.20  end;