changeset 12338 | de0f4a63baa5 |
parent 12311 | ce5f9e61c037 |
child 12480 | 32e67277a4b9 |
--- 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;