1.1 --- a/src/HOL/Divides.ML	Wed Aug 19 10:26:02 1998 +0200
     1.2 +++ b/src/HOL/Divides.ML	Wed Aug 19 10:26:37 1998 +0200
     1.3 @@ -228,7 +228,6 @@
     1.4   by (subgoal_tac "(m-n) div n < (m-n)" 1);
     1.5    by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
     1.6    by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
     1.7 - by (dres_inst_tac [("m","n")] less_imp_diff_positive 1);
     1.8   by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
     1.9  (* case n=m *)
    1.10  by (subgoal_tac "m=n" 1);