author | haftmann |
Fri, 23 Feb 2007 08:39:22 +0100 | |
changeset 22349 | a4e82dd93202 |
parent 22348 | ab505d281015 |
child 22350 | b410755a0d5a |
--- 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;