src/ZF/int_arith.ML

 
 (*combine unary minus with numeric literals, however nested within a product*)
 val int_mult_minus_simps =
     [@{thm zmult_assoc}, @{thm zmult_zminus} RS sym, int_minus_mult_eq_1_to_2];
 
-fun prep_simproc (name, pats, proc) =
-  Simplifier.simproc (the_context ()) name pats proc;
+fun prep_simproc thy (name, pats, proc) =
+  Simplifier.simproc thy name pats proc;
 
 structure CancelNumeralsCommon =
   struct
   val mk_sum            = (fn T:typ => mk_sum)
   val dest_sum          = dest_sum

   val bal_add1 = @{thm le_add_iff1} RS iff_trans
   val bal_add2 = @{thm le_add_iff2} RS iff_trans
 );
 
 val cancel_numerals =
-  map prep_simproc
+  map (prep_simproc @{theory})
    [("inteq_cancel_numerals",
      ["l $+ m = n", "l = m $+ n",
       "l $- m = n", "l = m $- n",
       "l $* m = n", "l = m $* n"],
      K EqCancelNumerals.proc),

   end;
 
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
 
 val combine_numerals =
-  prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc);
+  prep_simproc @{theory}
+    ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc);
 
 
 
 (** Constant folding for integer multiplication **)
 

 
 
 structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
 
 val combine_numerals_prod =
-  prep_simproc ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc);
+  prep_simproc @{theory}
+    ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc);
 
 end;
 
 
 Addsimprocs Int_Numeral_Simprocs.cancel_numerals;