# HG changeset patch
# User berghofe
# Date 1033463845 -7200
# Node ID 0b91269c0b13be62d9b718aaf26607e56aada902
# Parent  531f1f524848bd67cb410abd037c05132b990bf8
Deleted superfluous dest_implies.

diff -r 531f1f524848 -r 0b91269c0b13 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Sep 30 16:50:39 2002 +0200
+++ b/src/Pure/meta_simplifier.ML	Tue Oct 01 11:17:25 2002 +0200
@@ -742,9 +742,7 @@
                 | None => None
              end
          | t $ _ => (case t of
-             Const ("==>", _) $ _  =>
-               let val (s, u) = Drule.dest_implies t0
-               in impc t0 mss end
+             Const ("==>", _) $ _  => impc t0 mss
            | Abs _ =>
                let val thm = beta_conversion false t0
                in case subc skel0 mss (rhs_of thm) of