src/HOL/OrderedGroup.thy

--- a/src/HOL/OrderedGroup.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/OrderedGroup.thy	Wed Jul 15 23:48:21 2009 +0200
@@ -1380,7 +1380,7 @@
         if termless_agrp (y, x) then SOME ac2 else NONE
     | solve_add_ac thy _ _ = NONE
 in
-  val add_ac_proc = Simplifier.simproc (the_context ())
+  val add_ac_proc = Simplifier.simproc @{theory}
     "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
 end;