--- a/src/HOL/Tools/Qelim/presburger.ML Sun May 09 22:51:11 2010 -0700
+++ b/src/HOL/Tools/Qelim/presburger.ML Mon May 10 12:25:49 2010 +0200
@@ -10,7 +10,6 @@
structure Presburger : PRESBURGER =
struct
-open Conv;
val comp_ss = HOL_ss addsimps @{thms semiring_norm};
fun strip_objimp ct =
@@ -152,7 +151,7 @@
if !quick_and_dirty
then linzqe_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
(Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
- else arg_conv (Cooper.cooper_conv ctxt) p
+ else Conv.arg_conv (Cooper.cooper_conv ctxt) p
val p' = Thm.rhs_of cpth
val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
in rtac th i end