src/HOL/Product_Type.thy
changeset 22577 1a08fce38565
parent 22439 b709739c69e6
child 22744 5cbe966d67a2
     1.1 --- a/src/HOL/Product_Type.thy	Tue Apr 03 19:31:48 2007 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Apr 04 00:10:59 2007 +0200
     1.3 @@ -433,10 +433,8 @@
     1.4          | NONE => NONE)
     1.5    |   eta_proc _ _ = NONE;
     1.6  in
     1.7 -  val split_beta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
     1.8 -    "split_beta" ["split f z"] (K beta_proc);
     1.9 -  val split_eta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
    1.10 -    "split_eta" ["split f"] (K eta_proc);
    1.11 +  val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
    1.12 +  val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
    1.13  end;
    1.14  
    1.15  Addsimprocs [split_beta_proc, split_eta_proc];