changeset 28262 | aa7ca36d67fd |
parent 28130 | 32b4185bfdc7 |
child 28823 | dcbef866c9e2 |
--- 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;