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