# HG changeset patch
# User haftmann
# Date 1120467850 -7200
# Node ID f83f3aef274d1cae002538c503b28f2f7a1fc09a
# Parent  ca316edcb03160ab16639426182249bdb9cecec4
(intermediate commit)

diff -r ca316edcb031 -r f83f3aef274d src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sat Jul 02 13:08:28 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Mon Jul 04 11:04:10 2005 +0200
@@ -286,10 +286,10 @@
   (#1 o PureThy.add_thmss [(("simps", simps), []),
     (("", List.concat case_thms @ size_thms @ 
           List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
-    (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
+    (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
     (("", List.concat inject),               [iff_add_global]),
     (("", List.concat distinct RL [notE]),   [Classical.safe_elim_global]),
-    (("", weak_case_congs),           [cong_att])]);
+    (("", weak_case_congs),                  [cong_att])]);
 
 
 (* add_cases_induct *)