changeset 32010 | cb1a1c94b4cd |
parent 31001 | 7e6ffd8f51a9 |
child 32449 | 696d64ed85da |
--- a/src/HOL/Algebra/abstract/Ring2.thy Wed Jul 15 23:11:57 2009 +0200 +++ b/src/HOL/Algebra/abstract/Ring2.thy Wed Jul 15 23:48:21 2009 +0200 @@ -286,7 +286,7 @@ else SOME rew end; in - val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc); + val ring_simproc = Simplifier.simproc @{theory} "ring" lhss (K proc); end; *}