src/HOL/Product_Type.thy
changeset 43595 7ae4a23b5be6
parent 43594 ef1ddc59b825
child 43654 3f1a44c2d645
     1.1 --- a/src/HOL/Product_Type.thy	Wed Jun 29 17:35:46 2011 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Jun 29 18:12:34 2011 +0200
     1.3 @@ -556,6 +556,7 @@
     1.4          if Pair_pat k i (t $ u) then incr_boundvars k arg
     1.5          else (subst arg k i t $ subst arg k i u)
     1.6      | subst arg k i t = t;
     1.7 +in
     1.8    fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
     1.9          (case split_pat beta_term_pat 1 t of
    1.10            SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
    1.11 @@ -566,13 +567,10 @@
    1.12            SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
    1.13          | NONE => NONE)
    1.14      | eta_proc _ _ = NONE;
    1.15 -in
    1.16 -  val split_beta_proc = Simplifier.simproc_global @{theory} "split_beta" ["split f z"] (K beta_proc);
    1.17 -  val split_eta_proc = Simplifier.simproc_global @{theory} "split_eta" ["split f"] (K eta_proc);
    1.18  end;
    1.19 -
    1.20 -Addsimprocs [split_beta_proc, split_eta_proc];
    1.21  *}
    1.22 +simproc_setup split_beta ("split f z") = {* fn _ => fn ss => fn ct => beta_proc ss (term_of ct) *}
    1.23 +simproc_setup split_eta ("split f") = {* fn _ => fn ss => fn ct => eta_proc ss (term_of ct) *}
    1.24  
    1.25  lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
    1.26    by (subst surjective_pairing, rule split_conv)