# HG changeset patch
# User blanchet
# Date 1234775610 -3600
# Node ID ae8f42c245b2386dbaaf306d34f109c1b41ae15f
# Parent  7dac794eec91d59c78c3f50b42e7f6d6536ff83b
Added nitpick attribute, and fixed typo.

diff -r 7dac794eec91 -r ae8f42c245b2 src/HOL/List.thy
--- 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.
 *}
 
diff -r 7dac794eec91 -r ae8f42c245b2 src/HOL/Tools/datatype_abs_proofs.ML
--- 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))