changeset 12338 | de0f4a63baa5 |
parent 12196 | a3be6b3a9c0b |
child 12949 | b94843ffc0d1 |
--- 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;