changeset 14204 | 2fa6ecb87d47 |
parent 14184 | 2e0e02d68cbb |
child 14223 | 0ee05eef881b |
--- a/src/Pure/theory.ML Tue Sep 23 15:49:17 2003 +0200 +++ b/src/Pure/theory.ML Tue Sep 23 20:37:45 2003 +0200 @@ -316,7 +316,7 @@ (* clash_defns *) fun clash_defn c_ty (name, tm) = - let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in + let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals (Logic.strip_imp_concl tm)))) in if clash_consts c_ty (c, ty') then Some (name, ty') else None end handle TERM _ => None;