src/ZF/OrdQuant.thy
changeset 32010 cb1a1c94b4cd
parent 28262 aa7ca36d67fd
child 35112 ff6f60e6ab85
     1.1 --- a/src/ZF/OrdQuant.thy	Wed Jul 15 23:11:57 2009 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Wed Jul 15 23:48:21 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      ZF/AC/OrdQuant.thy
     1.5 -    ID:         $Id$
     1.6      Authors:    Krzysztof Grabczewski and L C Paulson
     1.7  *)
     1.8  
     1.9 @@ -382,9 +381,9 @@
    1.10  
    1.11  in
    1.12  
    1.13 -val defREX_regroup = Simplifier.simproc (the_context ())
    1.14 +val defREX_regroup = Simplifier.simproc @{theory}
    1.15    "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
    1.16 -val defRALL_regroup = Simplifier.simproc (the_context ())
    1.17 +val defRALL_regroup = Simplifier.simproc @{theory}
    1.18    "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
    1.19  
    1.20  end;