1.1 --- a/src/HOL/Presburger.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -704,7 +704,7 @@
     1.4      have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
     1.5      also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)"
     1.6        using minus[THEN spec, of "x - i * d"]
     1.7 -      by (simp add:int_distrib Ring_and_Field.diff_diff_eq[symmetric])
     1.8 +      by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric])
     1.9      ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast
    1.10    qed
    1.11  qed