| changeset 38715 | 6513ea67d95d |
| parent 38522 | de7984a7172b |
| child 41777 | 1f7cbe39d425 |
--- a/src/ZF/Datatype_ZF.thy Wed Aug 25 18:19:04 2010 +0200 +++ b/src/ZF/Datatype_ZF.thy Wed Aug 25 18:36:22 2010 +0200 @@ -101,7 +101,7 @@ handle Match => NONE; - val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc; + val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc; end;