# HG changeset patch
# User wenzelm
# Date 1247694501 -7200
# Node ID cb1a1c94b4cdf835cfc35b40481603ad1d181c47
# Parent  fd3c60ad9155618c97fb91975bac1220377a2d6f
more antiquotations;

diff -r fd3c60ad9155 -r cb1a1c94b4cd src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/CCL/CCL.thy	Wed Jul 15 23:48:21 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",
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/CCL/Hered.thy
--- a/src/CCL/Hered.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/CCL/Hered.thy	Wed Jul 15 23:48:21 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)",
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/CCL/Term.thy
--- a/src/CCL/Term.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/CCL/Term.thy	Wed Jul 15 23:48:21 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'",
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/CCL/Type.thy
--- a/src/CCL/Type.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/CCL/Type.thy	Wed Jul 15 23:48:21 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)",
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/FOL/simpdata.ML	Wed Jul 15 23:48:21 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;
 
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Jul 15 23:48:21 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;
 *}
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Divides.thy	Wed Jul 15 23:48:21 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];
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/IntDiv.thy	Wed Jul 15 23:48:21 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];
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Wed Jul 15 23:48:21 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
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/List.thy	Wed Jul 15 23:48:21 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;
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Modelcheck/EindhovenSyn.thy
--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Jul 15 23:48:21 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 =
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Wed Jul 15 23:48:21 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];
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 15 23:48:21 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";
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Jul 15 23:48:21 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 = 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/OrderedGroup.thy	Wed Jul 15 23:48:21 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;
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Product_Type.thy	Wed Jul 15 23:48:21 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];
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML	Wed Jul 15 23:48:21 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))" *)
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Set.thy	Wed Jul 15 23:48:21 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;
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Wed Jul 15 23:48:21 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';
 *}
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Wed Jul 15 23:48:21 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 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Wed Jul 15 23:48:21 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
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Wed Jul 15 23:48:21 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)];
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Jul 15 23:48:21 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*)
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/numeral.ML	Wed Jul 15 23:48:21 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)], []);
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Wed Jul 15 23:48:21 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 =
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Wed Jul 15 23:48:21 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 **)
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Wed Jul 15 23:48:21 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,  *)
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Tools/simpdata.ML	Wed Jul 15 23:48:21 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;
 
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOLCF/holcf_logic.ML
--- a/src/HOLCF/holcf_logic.ML	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOLCF/holcf_logic.ML	Wed Jul 15 23:48:21 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);
 
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/ZF/Datatype_ZF.thy	Wed Jul 15 23:48:21 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;
 
diff -r fd3c60ad9155 -r cb1a1c94b4cd src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/ZF/OrdQuant.thy	Wed Jul 15 23:48:21 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;