diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/arith_data.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -138,8 +138,7 @@
 
 (** prepare nat_cancel simprocs **)
 
-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;
 
 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;