--- a/src/HOL/Extraction/Pigeonhole.thy Tue Oct 31 14:58:14 2006 +0100
+++ b/src/HOL/Extraction/Pigeonhole.thy Tue Oct 31 14:58:16 2006 +0100
@@ -16,8 +16,8 @@
We need decidability of equality on natural numbers:
*}
-lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
- apply (induct m)
+lemma nat_eq_dec: "(m\<Colon>nat) = n \<or> m \<noteq> n"
+ apply (induct m arbitrary: n)
apply (case_tac n)
apply (case_tac [3] n)
apply (simp only: nat.simps, iprover?)+
@@ -307,9 +307,6 @@
arbitrary_nat_subst :: "nat \<times> nat"
"arbitrary_nat_subst = (0, 0)"
-lemma [code func]:
- "arbitrary_nat = arbitrary_nat" ..
-
code_axioms
arbitrary_nat \<equiv> arbitrary_nat_subst
@@ -317,7 +314,7 @@
"test n = pigeonhole n (\<lambda>m. m - 1)"
"test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
-code_gen test test' "op !" (SML -)
+code_gen test test' "op !" (SML *)
ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
--- a/src/HOL/Tools/datatype_package.ML Tue Oct 31 14:58:14 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Tue Oct 31 14:58:16 2006 +0100
@@ -305,13 +305,14 @@
fun add_rules simps case_thms size_thms rec_thms inject distinct
weak_case_congs cong_att =
- (snd o PureThy.add_thmss [(("simps", simps), []),
+ PureThy.add_thmss [(("simps", simps), []),
(("", flat case_thms @ size_thms @
flat distinct @ rec_thms), [Simplifier.simp_add]),
- (("", size_thms @ rec_thms), [setmp CodegenData.strict_functyp false (RecfunCodegen.add NONE)]),
- (("", flat inject), [iff_add]),
- (("", map name_notE (flat distinct)), [Classical.safe_elim NONE]),
- (("", weak_case_congs), [cong_att])]);
+ (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
+ (("", flat inject), [iff_add]),
+ (("", map name_notE (flat distinct)), [Classical.safe_elim NONE]),
+ (("", weak_case_congs), [cong_att])]
+ #> snd;
(* add_cases_induct *)