src/HOL/Product_Type.thy
changeset 13462 56610e2ba220
parent 12338 de0f4a63baa5
child 13480 bb72bd43c6c3
     1.1 --- a/src/HOL/Product_Type.thy	Tue Aug 06 11:20:47 2002 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Aug 06 11:22:05 2002 +0200
     1.3 @@ -29,13 +29,11 @@
     1.4  *}
     1.5  
     1.6  ML_setup {*
     1.7 -  local
     1.8 -    val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT));
     1.9 -    val unit_meta_eq = standard (mk_meta_eq (thm "unit_eq"));
    1.10 -    fun proc _ _ t =
    1.11 -      if HOLogic.is_unit t then None
    1.12 -      else Some unit_meta_eq
    1.13 -  in val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc end;
    1.14 +  val unit_eq_proc =
    1.15 +    let val unit_meta_eq = mk_meta_eq (thm "unit_eq") in
    1.16 +      Simplifier.simproc (Theory.sign_of (the_context ())) "unit_eq" ["x::unit"]
    1.17 +      (fn _ => fn _ => fn t => if HOLogic.is_unit t then None else Some unit_meta_eq)
    1.18 +    end;
    1.19  
    1.20    Addsimprocs [unit_eq_proc];
    1.21  *}
    1.22 @@ -341,12 +339,7 @@
    1.23    fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
    1.24          (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
    1.25          (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
    1.26 -  val sign = sign_of (the_context ());
    1.27 -  fun simproc name patstr =
    1.28 -    Simplifier.mk_simproc name [HOLogic.read_cterm sign patstr];
    1.29  
    1.30 -  val beta_patstr = "split f z";
    1.31 -  val  eta_patstr = "split f";
    1.32    fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
    1.33    |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
    1.34                          (beta_term_pat k i t andalso beta_term_pat k i u)
    1.35 @@ -368,8 +361,10 @@
    1.36          | None => None)
    1.37    |   eta_proc _ _ _ = None;
    1.38  in
    1.39 -  val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
    1.40 -  val split_eta_proc  = simproc "split_eta"   eta_patstr  eta_proc;
    1.41 +  val split_beta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
    1.42 +    "split_beta" ["split f z"] beta_proc;
    1.43 +  val split_eta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
    1.44 +    "split_eta" ["split f"] eta_proc;
    1.45  end;
    1.46  
    1.47  Addsimprocs [split_beta_proc, split_eta_proc];