simproc_setup fun_upd2;

--- a/src/HOL/Fun.thy	Sat Jul 28 20:40:18 2007 +0200
+++ b/src/HOL/Fun.thy	Sat Jul 28 20:40:19 2007 +0200
@@ -465,10 +465,10 @@
 text {* simplifies terms of the form
   f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *}
 
-ML {*
+simproc_setup fun_upd2 ("f(v := w, x := y)") = {* fn _ =>
 let
   fun gen_fun_upd NONE T _ _ = NONE
-    | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd},T) $ f $ x $ y)
+    | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd}, T) $ f $ x $ y)
   fun dest_fun_T1 (Type (_, T :: Ts)) = T
   fun find_double (t as Const (@{const_name fun_upd},T) $ f $ x $ y) =
     let
@@ -476,20 +476,22 @@
             if v aconv x then SOME g else gen_fun_upd (find g) T v w
         | find t = NONE
     in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
-  fun fun_upd_prover ss =
-    rtac eq_reflection 1 THEN rtac ext 1 THEN
-    simp_tac (Simplifier.inherit_context ss @{simpset}) 1
-  val fun_upd2_simproc =
-    Simplifier.simproc @{theory}
-      "fun_upd2" ["f(v := w, x := y)"]
-      (fn _ => fn ss => fn t =>
-        case find_double t of (T, NONE) => NONE
-        | (T, SOME rhs) =>
-            SOME (Goal.prove (Simplifier.the_context ss) [] []
-              (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
-in
-  Addsimprocs [fun_upd2_simproc]
-end;
+
+  fun proc ss ct =
+    let
+      val ctxt = Simplifier.the_context ss
+      val t = Thm.term_of ct
+    in
+      case find_double t of
+        (T, NONE) => NONE
+      | (T, SOME rhs) =>
+          SOME (Goal.prove ctxt [] [] (Term.equals T $ t $ rhs)
+            (fn _ =>
+              rtac eq_reflection 1 THEN
+              rtac ext 1 THEN
+              simp_tac (Simplifier.inherit_context ss @{simpset}) 1))
+    end
+in proc end
 *}