# HG changeset patch
# User blanchet
# Date 1271151791 -7200
# Node ID 00d550b6cfd408515fdefe76cdbbb9aaab5392ac
# Parent  86b952fc31dab8bd963895c00b6118f4475e490f
cosmetics

diff -r 86b952fc31da -r 00d550b6cfd4 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue Apr 13 11:13:52 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Tue Apr 13 11:43:11 2010 +0200
@@ -1445,8 +1445,8 @@
     (\!\begin{aligned}[t]%
     & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
     & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
-The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
-even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
+The existence of a nonstandard model suggests that the induction hypothesis is not general enough or may even
+be wrong. See the Nitpick manual's ``Inductive Properties'' section for details (``\textit{isabelle doc nitpick}'').
 \postw
 
 Reading the Nitpick manual is a most excellent idea.
diff -r 86b952fc31da -r 00d550b6cfd4 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 13 11:13:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 13 11:43:11 2010 +0200
@@ -658,9 +658,9 @@
               ();
             if not standard andalso likely_in_struct_induct_step then
               print "The existence of a nonstandard model suggests that the \
-                    \induction hypothesis is not general enough or perhaps \
-                    \even wrong. See the \"Inductive Properties\" section of \
-                    \the Nitpick manual for details (\"isabelle doc nitpick\")."
+                    \induction hypothesis is not general enough or may even be \
+                    \wrong. See the Nitpick manual's \"Inductive Properties\" \
+                    \section for details (\"isabelle doc nitpick\")."
             else
               ();
             if has_syntactic_sorts orig_t then
diff -r 86b952fc31da -r 00d550b6cfd4 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 13 11:13:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 13 11:43:11 2010 +0200
@@ -1265,9 +1265,8 @@
     boring <> is_funky_typedef_name thy s andalso is_typedef thy s
   | is_typedef_axiom _ _ _ = false
 (* term -> bool *)
-fun is_class_axiom t =
-  (t |> Logic.strip_horn |> swap |> op :: |> map Logic.dest_of_class; true)
-  handle TERM _ => false
+val is_class_axiom =
+  Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
 
 (* Distinguishes between (1) constant definition axioms, (2) type arity and
    typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).