src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 41994 c567c860caf6
parent 41898 55d981e1232a
child 42361 23f352990944
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 17 22:07:17 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Mar 18 10:17:37 2011 +0100
     1.3 @@ -214,6 +214,7 @@
     1.4    val fixpoint_kind_of_const :
     1.5      theory -> const_table * const_table -> string * typ -> fixpoint_kind
     1.6    val is_real_inductive_pred : hol_context -> styp -> bool
     1.7 +  val is_constr_pattern : Proof.context -> term -> bool
     1.8    val is_constr_pattern_lhs : Proof.context -> term -> bool
     1.9    val is_constr_pattern_formula : Proof.context -> term -> bool
    1.10    val nondef_props_for_const :