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];