--- a/src/HOL/Fun.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Fun.ML Sat Dec 01 18:52:32 2001 +0100
@@ -373,7 +373,7 @@
fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r)
in
val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2"
- [Thm.read_cterm (sign_of (the_context ())) ("f(v:=w,x:=y)", HOLogic.termT)]
+ [HOLogic.read_cterm (sign_of (the_context ())) "f(v := w, x := y)"]
(fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=>
Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover))))
end;