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