--- a/src/ZF/arith_data.ML Wed May 15 13:50:38 2002 +0200
+++ b/src/ZF/arith_data.ML Thu May 16 09:16:22 2002 +0200
@@ -175,8 +175,8 @@
struct
open CancelNumeralsCommon
val prove_conv = prove_conv "natless_cancel_numerals"
- val mk_bal = FOLogic.mk_binrel "Ordinal.op <"
- val dest_bal = FOLogic.dest_bin "Ordinal.op <" iT
+ val mk_bal = FOLogic.mk_binrel "Ordinal.lt"
+ val dest_bal = FOLogic.dest_bin "Ordinal.lt" iT
val bal_add1 = less_add_iff RS iff_trans
val bal_add2 = less_add_iff RS iff_trans
val trans_tac = gen_trans_tac iff_trans