src/Pure/theory.ML

 
 
 (* 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;
 
 fun clash_defns c_ty axms =
   distinct (mapfilter (clash_defn c_ty) axms);