changeset 18338 | ed2d0e60fbcc |
parent 18139 | b15981aedb7b |
child 18678 | dd0c569fa43d |
--- a/src/Pure/theory.ML Fri Dec 02 22:54:45 2005 +0100 +++ b/src/Pure/theory.ML Fri Dec 02 22:54:47 2005 +0100 @@ -260,7 +260,7 @@ val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm) handle TERM _ => err "Not a meta-equality (==)"; - val (head, args) = Term.strip_comb lhs; + val (head, args) = Term.strip_comb (Pattern.beta_eta_contract lhs); val (c, T) = Term.dest_Const head handle TERM _ => err "Head of lhs not a constant";