src/Pure/theory.ML
changeset 14204 2fa6ecb87d47
parent 14184 2e0e02d68cbb
child 14223 0ee05eef881b
equal deleted inserted replaced
14203:97df98601d23 14204:2fa6ecb87d47
   314 
   314 
   315 
   315 
   316 (* clash_defns *)
   316 (* clash_defns *)
   317 
   317 
   318 fun clash_defn c_ty (name, tm) =
   318 fun clash_defn c_ty (name, tm) =
   319   let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in
   319   let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals (Logic.strip_imp_concl tm)))) in
   320     if clash_consts c_ty (c, ty') then Some (name, ty') else None
   320     if clash_consts c_ty (c, ty') then Some (name, ty') else None
   321   end handle TERM _ => None;
   321   end handle TERM _ => None;
   322 
   322 
   323 fun clash_defns c_ty axms =
   323 fun clash_defns c_ty axms =
   324   distinct (mapfilter (clash_defn c_ty) axms);
   324   distinct (mapfilter (clash_defn c_ty) axms);