Deleted superfluous dest_implies.

--- 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