diff -r 045187fc7840 -r aa7ca36d67fd src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/OrderedGroup.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -1390,7 +1390,7 @@
         if termless_agrp (y, x) then SOME ac2 else NONE
     | solve_add_ac thy _ _ = NONE
 in
-  val add_ac_proc = Simplifier.simproc @{theory}
+  val add_ac_proc = Simplifier.simproc (the_context ())
     "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
 end;