# HG changeset patch
# User haftmann
# Date 1241762469 -7200
# Node ID fd7ec31f850cce843722f0afeb9bc16a6a8ef91c
# Parent  972c870da225b5d9d8aba39134416f55d5ac7455
generalized simproc for mod

diff -r 972c870da225 -r fd7ec31f850c src/HOL/Tools/int_factor_simprocs.ML
--- a/src/HOL/Tools/int_factor_simprocs.ML	Fri May 08 08:00:13 2009 +0200
+++ b/src/HOL/Tools/int_factor_simprocs.ML	Fri May 08 08:01:09 2009 +0200
@@ -222,7 +222,7 @@
     simplify_one ss (([th, cancel_th]) MRS trans);
 
 local
-  val Tp_Eq = Thm.reflexive(Thm.cterm_of (@{theory HOL}) HOLogic.Trueprop)
+  val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop)
   fun Eq_True_elim Eq = 
     Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
 in
@@ -297,7 +297,7 @@
  (open CancelFactorCommon
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
-  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
   val simp_conv = K (K (SOME @{thm mod_mult_mult1}))
 );