src/HOL/Tools/nat_numeral_simprocs.ML
changeset 32155 e2bf2f73b0c8
parent 32010 cb1a1c94b4cd
child 34974 18b41bba42b5
     1.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Jul 23 22:20:37 2009 +0200
     1.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Jul 23 23:12:21 2009 +0200
     1.3 @@ -202,7 +202,7 @@
     1.4  
     1.5  
     1.6  val cancel_numerals =
     1.7 -  map Arith_Data.prep_simproc
     1.8 +  map (Arith_Data.prep_simproc @{theory})
     1.9     [("nateq_cancel_numerals",
    1.10       ["(l::nat) + m = n", "(l::nat) = m + n",
    1.11        "(l::nat) * m = n", "(l::nat) = m * n",
    1.12 @@ -254,7 +254,8 @@
    1.13  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
    1.14  
    1.15  val combine_numerals =
    1.16 -  Arith_Data.prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
    1.17 +  Arith_Data.prep_simproc @{theory}
    1.18 +    ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
    1.19  
    1.20  
    1.21  (*** Applying CancelNumeralFactorFun ***)
    1.22 @@ -323,7 +324,7 @@
    1.23  )
    1.24  
    1.25  val cancel_numeral_factors =
    1.26 -  map Arith_Data.prep_simproc
    1.27 +  map (Arith_Data.prep_simproc @{theory})
    1.28     [("nateq_cancel_numeral_factors",
    1.29       ["(l::nat) * m = n", "(l::nat) = m * n"],
    1.30       K EqCancelNumeralFactor.proc),
    1.31 @@ -416,7 +417,7 @@
    1.32  );
    1.33  
    1.34  val cancel_factor =
    1.35 -  map Arith_Data.prep_simproc
    1.36 +  map (Arith_Data.prep_simproc @{theory})
    1.37     [("nat_eq_cancel_factor",
    1.38       ["(l::nat) * m = n", "(l::nat) = m * n"],
    1.39       K EqCancelFactor.proc),