changeset 32010 | cb1a1c94b4cd |
parent 31902 | 862ae16a799d |
child 32075 | e8e0fb5da77a |
--- 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;