Added nitpick attribute, and fixed typo.

--- a/src/HOL/List.thy	Mon Feb 16 10:11:20 2009 +0100
+++ b/src/HOL/List.thy	Mon Feb 16 10:13:30 2009 +0100
@@ -257,7 +257,7 @@
 \caption{Characteristic examples}
 \label{fig:Characteristic}
 \end{figure}
-Figure~\ref{fig:Characteristic} shows charachteristic examples
+Figure~\ref{fig:Characteristic} shows characteristic examples
 that should give an intuitive understanding of the above functions.
 *}
 

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Feb 16 10:11:20 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Feb 16 10:13:30 2009 +0100
@@ -262,7 +262,8 @@
   in
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
-    |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [])]
+    |> PureThy.add_thmss [((Binding.name "recs", rec_thms),
+         [Nitpick_Const_Simp_Thms.add])]
     ||> Sign.parent_path
     ||> Theory.checkpoint
     |-> (fn thms => pair (reccomb_names, Library.flat thms))