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