src/ZF/OrdQuant.thy
changeset 26480 544cef16045b
parent 26339 7825c83c9eff
child 28262 aa7ca36d67fd
     1.1 --- a/src/ZF/OrdQuant.thy	Sat Mar 29 19:13:58 2008 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Sat Mar 29 19:14:00 2008 +0100
     1.3 @@ -369,7 +369,7 @@
     1.4  
     1.5  text {* Setting up the one-point-rule simproc *}
     1.6  
     1.7 -ML_setup {*
     1.8 +ML {*
     1.9  local
    1.10  
    1.11  val unfold_rex_tac = unfold_tac [@{thm rex_def}];