changeset 32010 | cb1a1c94b4cd |
parent 32007 | a2a3685f61c3 |
child 32075 | e8e0fb5da77a |
--- a/src/HOL/List.thy Wed Jul 15 23:11:57 2009 +0200 +++ b/src/HOL/List.thy Wed Jul 15 23:48:21 2009 +0200 @@ -679,7 +679,7 @@ in val list_eq_simproc = - Simplifier.simproc (the_context ()) "list_eq" ["(xs::'a list) = ys"] (K list_eq); + Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq); end;