diff -r c48defc2b28c -r 342029af73d1 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Mon Jun 25 00:36:36 2007 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Mon Jun 25 00:36:37 2007 +0200
@@ -148,7 +148,7 @@
    NONE => no_tac st
  | SOME p => 
    let
-    val eq = (eta_conv (ProofContext.theory_of ctxt) then_conv Thm.beta_conversion true) p
+    val eq = (Thm.eta_long_conversion then_conv Thm.beta_conversion true) p
     val p' = Thm.rhs_of eq
     val th = implies_intr p' (equal_elim (symmetric eq) (assume p'))
    in rtac th i st