Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/int_factor_simprocs.ML
changeset 31067 fd7ec31f850c
parent 30931 86ca651da03e 
--- 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}))
 );
isabelle