--- a/src/HOL/Tools/Qelim/qelim.ML Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML Thu Oct 31 11:44:20 2013 +0100
@@ -37,7 +37,7 @@
val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
|> Drule.arg_cong_rule e
val th' = simpex_conv (Thm.rhs_of th)
- val (l,r) = Thm.dest_equals (cprop_of th')
+ val (_, r) = Thm.dest_equals (cprop_of th')
in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
else Thm.transitive (Thm.transitive th th') (conv env r) end
| Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p