slight cleanup
authorhaftmann
Fri Feb 23 08:39:22 2007 +0100 (2007-02-23)
changeset 22349a4e82dd93202
parent 22348 ab505d281015
child 22350 b410755a0d5a
slight cleanup
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Fri Feb 23 08:39:21 2007 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Feb 23 08:39:22 2007 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4  ML_setup {*
     1.5    val unit_eq_proc =
     1.6      let val unit_meta_eq = mk_meta_eq (thm "unit_eq") in
     1.7 -      Simplifier.simproc (Theory.sign_of (the_context ())) "unit_eq" ["x::unit"]
     1.8 +      Simplifier.simproc (the_context ()) "unit_eq" ["x::unit"]
     1.9        (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
    1.10      end;
    1.11