src/HOL/Product_Type.thy

   |   no_args k i (Bound m) = m < k orelse m > k+i
   |   no_args _ _ _ = true;
   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)));
 
   fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
   |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse

   |    eta_term_pat _ _ _ = false;
   fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
   |   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];
 *}