diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -169,8 +169,7 @@
                 bin_arith_simps @ bin_rel_simps;
 
 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
-                                (s, HOLogic.termT);
+fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
 val prep_pats = map prep_pat;