changeset 32010 | cb1a1c94b4cd |
parent 31790 | 05c92381363c |
child 32155 | e2bf2f73b0c8 |
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Wed Jul 15 23:11:57 2009 +0200 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Wed Jul 15 23:48:21 2009 +0200 @@ -19,7 +19,7 @@ val numeral_sym_ss = HOL_ss addsimps numeral_syms; fun rename_numerals th = - simplify numeral_sym_ss (Thm.transfer (the_context ()) th); + simplify numeral_sym_ss (Thm.transfer @{theory} th); (*Utilities*)