src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46320 0b8b73b49848
parent 46244 549755ebf4d2
child 46745 a6f83f21dc2c
equal deleted inserted replaced
46319:c248e4f1be74 46320:0b8b73b49848
  1010                   else
  1010                   else
  1011                     card_of_type assigns T
  1011                     card_of_type assigns T
  1012                     handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
  1012                     handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
  1013                            default_card)
  1013                            default_card)
  1014 
  1014 
  1015 (* Similar to "ATP_Translate.tiny_card_of_type". *)
  1015 (* Similar to "ATP_Util.tiny_card_of_type". *)
  1016 fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
  1016 fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
  1017                                assigns T =
  1017                                assigns T =
  1018   let
  1018   let
  1019     fun aux avoid T =
  1019     fun aux avoid T =
  1020       (if member (op =) avoid T then
  1020       (if member (op =) avoid T then