# HG changeset patch
# User haftmann
# Date 1172216362 -3600
# Node ID a4e82dd93202a760989a6b67f11332956181a577
# Parent  ab505d2810154458a40c5a13dfccfcdffdeab6de
slight cleanup

diff -r ab505d281015 -r a4e82dd93202 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;