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