cosmetics
authorblanchet
Tue, 13 Apr 2010 11:43:11 +0200
changeset 36126 00d550b6cfd4
parent 36121 86b952fc31da
child 36127 e91292c520be
cosmetics
doc-src/Nitpick/nitpick.tex
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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.
--- 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
--- 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)).