src/HOL/Integ/int_arith2.ML

--- a/src/HOL/Integ/int_arith2.ML	Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Integ/int_arith2.ML	Wed Aug 30 16:29:21 2000 +0200
@@ -88,7 +88,7 @@
 
 (*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
 Goal "n<=m --> int m - int n = int (m-n)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (induct_thm_tac diff_induct "m n" 1);
 by Auto_tac;
 qed_spec_mp "zdiff_int";