1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Apr 13 11:13:52 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Apr 13 11:43:11 2010 +0200
     1.3 @@ -1445,8 +1445,8 @@
     1.4      (\!\begin{aligned}[t]%
     1.5      & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
     1.6      & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
     1.7 -The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
     1.8 -even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
     1.9 +The existence of a nonstandard model suggests that the induction hypothesis is not general enough or may even
    1.10 +be wrong. See the Nitpick manual's ``Inductive Properties'' section for details (``\textit{isabelle doc nitpick}'').
    1.11  \postw
    1.12  
    1.13  Reading the Nitpick manual is a most excellent idea.

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 13 11:13:52 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 13 11:43:11 2010 +0200
     2.3 @@ -658,9 +658,9 @@
     2.4                ();
     2.5              if not standard andalso likely_in_struct_induct_step then
     2.6                print "The existence of a nonstandard model suggests that the \
     2.7 -                    \induction hypothesis is not general enough or perhaps \
     2.8 -                    \even wrong. See the \"Inductive Properties\" section of \
     2.9 -                    \the Nitpick manual for details (\"isabelle doc nitpick\")."
    2.10 +                    \induction hypothesis is not general enough or may even be \
    2.11 +                    \wrong. See the Nitpick manual's \"Inductive Properties\" \
    2.12 +                    \section for details (\"isabelle doc nitpick\")."
    2.13              else
    2.14                ();
    2.15              if has_syntactic_sorts orig_t then

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 13 11:13:52 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 13 11:43:11 2010 +0200
     3.3 @@ -1265,9 +1265,8 @@
     3.4      boring <> is_funky_typedef_name thy s andalso is_typedef thy s
     3.5    | is_typedef_axiom _ _ _ = false
     3.6  (* term -> bool *)
     3.7 -fun is_class_axiom t =
     3.8 -  (t |> Logic.strip_horn |> swap |> op :: |> map Logic.dest_of_class; true)
     3.9 -  handle TERM _ => false
    3.10 +val is_class_axiom =
    3.11 +  Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
    3.12  
    3.13  (* Distinguishes between (1) constant definition axioms, (2) type arity and
    3.14     typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).