--- a/src/HOL/Product_Type.thy Sat Jul 08 12:54:29 2006 +0200
+++ b/src/HOL/Product_Type.thy Sat Jul 08 12:54:30 2006 +0200
@@ -407,7 +407,7 @@
fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE
| split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
| split_pat tp i _ = NONE;
- fun metaeq thy ss lhs rhs = mk_meta_eq (Goal.prove thy [] []
+ fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
(K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 1)));
@@ -421,21 +421,21 @@
| subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
else (subst arg k i t $ subst arg k i u)
| subst arg k i t = t;
- fun beta_proc thy ss (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
+ fun beta_proc ss (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
(case split_pat beta_term_pat 1 t of
- SOME (i,f) => SOME (metaeq thy ss s (subst arg 0 i f))
+ SOME (i,f) => SOME (metaeq ss s (subst arg 0 i f))
| NONE => NONE)
- | beta_proc _ _ _ = NONE;
- fun eta_proc thy ss (s as Const ("split", _) $ Abs (_, _, t)) =
+ | beta_proc _ _ = NONE;
+ fun eta_proc ss (s as Const ("split", _) $ Abs (_, _, t)) =
(case split_pat eta_term_pat 1 t of
- SOME (_,ft) => SOME (metaeq thy ss s (let val (f $ arg) = ft in f end))
+ SOME (_,ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
| NONE => NONE)
- | eta_proc _ _ _ = NONE;
+ | eta_proc _ _ = NONE;
in
val split_beta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
- "split_beta" ["split f z"] beta_proc;
+ "split_beta" ["split f z"] (K beta_proc);
val split_eta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
- "split_eta" ["split f"] eta_proc;
+ "split_eta" ["split f"] (K eta_proc);
end;
Addsimprocs [split_beta_proc, split_eta_proc];