changeset 13614 | 0b91269c0b13 |
parent 13607 | 6908230623a3 |
child 13661 | ec97dfc2bfe0 |
--- 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