--- a/src/HOL/Integ/int_factor_simprocs.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML Sat Nov 18 00:20:24 2006 +0100
@@ -64,8 +64,8 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "Divides.op div"
- val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
+ val mk_bal = HOLogic.mk_binop "Divides.div"
+ val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.intT
val cancel = int_mult_div_cancel1 RS trans
val neg_exchanges = false
)
@@ -272,8 +272,8 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "Divides.op div"
- val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
+ val mk_bal = HOLogic.mk_binop "Divides.div"
+ val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.intT
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_div_cancel_disj
);