src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Fri Feb 23 08:39:21 2007 +0100
+++ b/src/HOL/Product_Type.thy	Fri Feb 23 08:39:22 2007 +0100
@@ -33,7 +33,7 @@
 ML_setup {*
   val unit_eq_proc =
     let val unit_meta_eq = mk_meta_eq (thm "unit_eq") in
-      Simplifier.simproc (Theory.sign_of (the_context ())) "unit_eq" ["x::unit"]
+      Simplifier.simproc (the_context ()) "unit_eq" ["x::unit"]
       (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
     end;