diff -r 08d52e2dba07 -r c2e15e65165f src/HOL/MetisExamples/BigO.thy
--- a/src/HOL/MetisExamples/BigO.thy	Mon Feb 04 17:00:01 2008 +0100
+++ b/src/HOL/MetisExamples/BigO.thy	Wed Feb 06 08:34:32 2008 +0100
@@ -389,11 +389,11 @@
 have 4: "\<And>X1 X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
   by (metis linorder_linear abs_le_D1)
 have 5: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
-  by (metis abs_mult_self AC_mult.f.commute)
+  by (metis abs_mult_self)
 have 6: "\<And>X3. \<not> X3 * X3 < (0\<Colon>'b\<Colon>ordered_idom)"
-  by (metis not_square_less_zero AC_mult.f.commute)
+  by (metis not_square_less_zero)
 have 7: "\<And>X1 X3::'b. \<bar>X1\<bar> * \<bar>X3\<bar> = \<bar>X3 * X1\<bar>"
-  by (metis abs_mult AC_mult.f.commute)
+  by (metis abs_mult mult_commute)
 have 8: "\<And>X3::'b. X3 * X3 = \<bar>X3 * X3\<bar>"
   by (metis abs_mult 5)
 have 9: "\<And>X3. X3 * g (x \<bar>X3\<bar>) \<le> f (x \<bar>X3\<bar>)"
@@ -403,7 +403,7 @@
 have 11: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
   by (metis abs_idempotent abs_mult 8)
 have 12: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
-  by (metis AC_mult.f.commute 7 11)
+  by (metis mult_commute 7 11)
 have 13: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = X3 * X3"
   by (metis 8 7 12)
 have 14: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> X3 < (0\<Colon>'b)"
@@ -597,8 +597,10 @@
       (c * abs(f x)) * (ca * abs(g x))")
 ML{*ResAtp.problem_name := "BigO__bigo_mult_simpler"*}
 prefer 2 
-apply (metis  Finite_Set.AC_mult.f.assoc  Finite_Set.AC_mult.f.left_commute  OrderedGroup.abs_of_pos  OrderedGroup.mult_left_commute  Ring_and_Field.abs_mult  Ring_and_Field.mult_pos_pos)
-  apply(erule ssubst) 
+apply (metis mult_assoc mult_left_commute
+  OrderedGroup.abs_of_pos OrderedGroup.mult_left_commute
+  Ring_and_Field.abs_mult Ring_and_Field.mult_pos_pos)
+  apply (erule ssubst) 
   apply (subst abs_mult)
 (*not qute BigO__bigo_mult_simpler_1 (a hard problem!) as abs_mult has
   just been done*)
@@ -627,7 +629,7 @@
 have 9: "\<And>X1\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>X1\<bar>"
   by (metis OrderedGroup.abs_ge_zero 5)
 have 10: "\<And>X1\<Colon>'b\<Colon>ordered_idom. X1 * (1\<Colon>'b\<Colon>ordered_idom) = X1"
-  by (metis Ring_and_Field.mult_cancel_right2 Finite_Set.AC_mult.f.commute)
+  by (metis Ring_and_Field.mult_cancel_right2 mult_commute)
 have 11: "\<And>X1\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar> * \<bar>1\<Colon>'b\<Colon>ordered_idom\<bar>"
   by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 10)
 have 12: "\<And>X1\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
@@ -901,10 +903,10 @@
   apply safe
   apply (rule_tac [2] ext) 
    prefer 2 
-   apply (metis AC_mult.f_e.left_ident mult_assoc right_inverse)
+   apply simp
   apply (simp add: mult_assoc [symmetric] abs_mult)
   (*couldn't get this proof without the step above; SLOW*)
-  apply (metis AC_mult.f.assoc abs_ge_zero mult_left_mono)
+  apply (metis mult_assoc abs_ge_zero mult_left_mono)
 done