src/HOL/Product_Type.thy
changeset 43594 ef1ddc59b825
parent 42411 ff997038e8eb
child 43595 7ae4a23b5be6
     1.1 --- a/src/HOL/Product_Type.thy	Wed Jun 29 16:31:50 2011 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Jun 29 17:35:46 2011 +0200
     1.3 @@ -55,14 +55,10 @@
     1.4    this rule directly --- it loops!
     1.5  *}
     1.6  
     1.7 -ML {*
     1.8 -  val unit_eq_proc =
     1.9 -    let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
    1.10 -      Simplifier.simproc_global @{theory} "unit_eq" ["x::unit"]
    1.11 -      (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
    1.12 -    end;
    1.13 -
    1.14 -  Addsimprocs [unit_eq_proc];
    1.15 +simproc_setup unit_eq ("x::unit") = {*
    1.16 +  fn _ => fn _ => fn ct =>
    1.17 +    if HOLogic.is_unit (term_of ct) then NONE
    1.18 +    else SOME (mk_meta_eq @{thm unit_eq})
    1.19  *}
    1.20  
    1.21  rep_datatype "()" by simp
    1.22 @@ -74,7 +70,7 @@
    1.23    by (rule triv_forall_equality)
    1.24  
    1.25  text {*
    1.26 -  This rewrite counters the effect of @{text unit_eq_proc} on @{term
    1.27 +  This rewrite counters the effect of simproc @{text unit_eq} on @{term
    1.28    [source] "%u::unit. f u"}, replacing it by @{term [source]
    1.29    f} rather than by @{term [source] "%u. f ()"}.
    1.30  *}
    1.31 @@ -497,7 +493,7 @@
    1.32        | exists_paired_all _ = false;
    1.33      val ss = HOL_basic_ss
    1.34        addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}]
    1.35 -      addsimprocs [unit_eq_proc];
    1.36 +      addsimprocs [@{simproc unit_eq}];
    1.37    in
    1.38      val split_all_tac = SUBGOAL (fn (t, i) =>
    1.39        if exists_paired_all t then safe_full_simp_tac ss i else no_tac);