--- a/src/HOL/Code_Evaluation.thy Thu Nov 12 14:47:54 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy Thu Nov 12 15:49:30 2009 +0100
@@ -145,7 +145,7 @@
(Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
code_const "term_of \<Colon> String.literal \<Rightarrow> term"
- (Eval "HOLogic.mk'_message'_string")
+ (Eval "HOLogic.mk'_literal")
code_reserved Eval HOLogic
--- a/src/HOL/Datatype.thy Thu Nov 12 14:47:54 2009 +0100
+++ b/src/HOL/Datatype.thy Thu Nov 12 15:49:30 2009 +0100
@@ -562,6 +562,14 @@
Sumr :: "('b => 'c) => 'a + 'b => 'c"
"Sumr == sum_case undefined"
+lemma [code]:
+ "Suml f (Inl x) = f x"
+ by (simp add: Suml_def)
+
+lemma [code]:
+ "Sumr f (Inr x) = f x"
+ by (simp add: Sumr_def)
+
lemma Suml_inject: "Suml f = Suml g ==> f = g"
by (unfold Suml_def) (erule sum_case_inject)