src/HOL/Product_Type.thy
changeset 38715 6513ea67d95d
parent 37808 e604e5f9bb6a
child 38857 97775f3e8722
     1.1 --- a/src/HOL/Product_Type.thy	Wed Aug 25 18:19:04 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Aug 25 18:36:22 2010 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4  ML {*
     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} "unit_eq" ["x::unit"]
     1.8 +      Simplifier.simproc_global @{theory} "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  
    1.12 @@ -550,8 +550,8 @@
    1.13          | NONE => NONE)
    1.14      | eta_proc _ _ = NONE;
    1.15  in
    1.16 -  val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
    1.17 -  val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
    1.18 +  val split_beta_proc = Simplifier.simproc_global @{theory} "split_beta" ["split f z"] (K beta_proc);
    1.19 +  val split_eta_proc = Simplifier.simproc_global @{theory} "split_eta" ["split f"] (K eta_proc);
    1.20  end;
    1.21  
    1.22  Addsimprocs [split_beta_proc, split_eta_proc];