src/ZF/arith_data.ML

--- a/src/ZF/arith_data.ML	Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/arith_data.ML	Sun Feb 28 22:30:51 2010 +0100
@@ -163,9 +163,9 @@
   val prove_conv = prove_conv "nateq_cancel_numerals"
   val mk_bal   = FOLogic.mk_eq
   val dest_bal = FOLogic.dest_eq
-  val bal_add1 = @{thm eq_add_iff} RS iff_trans
-  val bal_add2 = @{thm eq_add_iff} RS iff_trans
-  fun trans_tac _ = gen_trans_tac iff_trans
+  val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans}
+  val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans}
+  fun trans_tac _ = gen_trans_tac @{thm iff_trans}
   end;
 
 structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
@@ -176,9 +176,9 @@
   val prove_conv = prove_conv "natless_cancel_numerals"
   val mk_bal   = FOLogic.mk_binrel "Ordinal.lt"
   val dest_bal = FOLogic.dest_bin "Ordinal.lt" iT
-  val bal_add1 = @{thm less_add_iff} RS iff_trans
-  val bal_add2 = @{thm less_add_iff} RS iff_trans
-  fun trans_tac _ = gen_trans_tac iff_trans
+  val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
+  val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
+  fun trans_tac _ = gen_trans_tac @{thm iff_trans}
   end;
 
 structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
@@ -189,9 +189,9 @@
   val prove_conv = prove_conv "natdiff_cancel_numerals"
   val mk_bal   = FOLogic.mk_binop "Arith.diff"
   val dest_bal = FOLogic.dest_bin "Arith.diff" iT
-  val bal_add1 = @{thm diff_add_eq} RS trans
-  val bal_add2 = @{thm diff_add_eq} RS trans
-  fun trans_tac _ = gen_trans_tac trans
+  val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
+  val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
+  fun trans_tac _ = gen_trans_tac @{thm trans}
   end;
 
 structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);