# HG changeset patch
# User blanchet
# Date 1234775743 -3600
# Node ID 66c5cc1e60a9c72d4a5b41db629a9a24dc491d34
# Parent  17d1e32ef867ebe794bc504875f3de5595271283# Parent  ae8f42c245b2386dbaaf306d34f109c1b41ae15f
merged

diff -r 17d1e32ef867 -r 66c5cc1e60a9 Admin/isatest/isatest-settings
--- a/Admin/isatest/isatest-settings	Sun Feb 15 22:58:02 2009 +0100
+++ b/Admin/isatest/isatest-settings	Mon Feb 16 10:15:43 2009 +0100
@@ -11,7 +11,7 @@
 HOME=/home/isatest
 
 ## send email on failure to
-MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk makarius@sketis.net haftmann@in.tum.de krauss@in.tum.de"
+MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk makarius@sketis.net haftmann@in.tum.de krauss@in.tum.de blanchet@in.tum.de"
 
 LOGPREFIX=$HOME/log
 MASTERLOG=$LOGPREFIX/isatest.log
diff -r 17d1e32ef867 -r 66c5cc1e60a9 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Feb 15 22:58:02 2009 +0100
+++ b/src/HOL/List.thy	Mon Feb 16 10:15:43 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 17d1e32ef867 -r 66c5cc1e60a9 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Feb 15 22:58:02 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Feb 16 10:15:43 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))