ML antiquotes;

--- a/src/FOLP/FOLP.thy	Tue Apr 03 19:31:48 2007 +0200
+++ b/src/FOLP/FOLP.thy	Wed Apr 04 00:10:59 2007 +0200
@@ -38,15 +38,14 @@
   val imp_intr = impI
 
   (*etac rev_cut_eq moves an equality to be the last premise. *)
-  val rev_cut_eq = prove_goal (the_context ())
+  val rev_cut_eq = prove_goal @{theory}
                 "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
    (fn prems => [ REPEAT(resolve_tac prems 1) ]);
 
   val rev_mp = rev_mp
   val subst = subst
   val sym = sym
-  val thin_refl = prove_goal (the_context ())
-                  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
+  val thin_refl = prove_goal @{theory} "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
   end;
 
 structure Hypsubst = HypsubstFun(Hypsubst_Data);

--- a/src/HOL/Fun.thy	Tue Apr 03 19:31:48 2007 +0200
+++ b/src/HOL/Fun.thy	Wed Apr 04 00:10:59 2007 +0200
@@ -579,7 +579,7 @@
     simp_tac (Simplifier.inherit_context ss current_ss) 1
 in
   val fun_upd2_simproc =
-    Simplifier.simproc (Theory.sign_of (the_context ()))
+    Simplifier.simproc @{theory}
       "fun_upd2" ["f(v := w, x := y)"]
       (fn _ => fn ss => fn t =>
         case find_double t of (T, NONE) => NONE

--- a/src/HOL/Product_Type.thy	Tue Apr 03 19:31:48 2007 +0200
+++ b/src/HOL/Product_Type.thy	Wed Apr 04 00:10:59 2007 +0200
@@ -433,10 +433,8 @@
         | NONE => NONE)
   |   eta_proc _ _ = NONE;
 in
-  val split_beta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
-    "split_beta" ["split f z"] (K beta_proc);
-  val split_eta_proc = Simplifier.simproc (Theory.sign_of (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/HOLCF/Pcpo.thy	Tue Apr 03 19:31:48 2007 +0200
+++ b/src/HOLCF/Pcpo.thy	Wed Apr 04 00:10:59 2007 +0200
@@ -206,8 +206,7 @@
       | _ => SOME meta_UU_reorient;
 in
   val UU_reorient_simproc = 
-    Simplifier.simproc (the_context ())
-      "UU_reorient_simproc" ["UU=x"] reorient_proc
+    Simplifier.simproc @{theory} "UU_reorient_simproc" ["UU=x"] reorient_proc
 end;
 
 Addsimprocs [UU_reorient_simproc];