diff -r 6f43714517ee -r 08c8dad8e399 src/HOL/Tools/Presburger/qelim.ML
--- a/src/HOL/Tools/Presburger/qelim.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOL/Tools/Presburger/qelim.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -51,7 +51,7 @@
       end
 
    |(Const("All",_)$Abs(xn,xT,p)) => ([(HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p)], fn [th] => th RS qe_ALL)
-   | _ => ([],fn [] => instantiate' [Some (ctyp_of sg (type_of P))] [Some (cterm_of sg P)] refl);
+   | _ => ([],fn [] => instantiate' [SOME (ctyp_of sg (type_of P))] [SOME (cterm_of sg P)] refl);
  
 
 fun tproof_of_mlift_qelim sg isat afnp nfnp qfnp p =