--- a/src/HOL/Orderings.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Orderings.thy Tue Jul 14 10:54:04 2009 +0200
@@ -268,13 +268,13 @@
text {* Explicit dictionaries for code generation *}
-lemma min_ord_min [code, code unfold, code inline del]:
+lemma min_ord_min [code, code_unfold, code_inline del]:
"min = ord.min (op \<le>)"
by (rule ext)+ (simp add: min_def ord.min_def)
declare ord.min_def [code]
-lemma max_ord_max [code, code unfold, code inline del]:
+lemma max_ord_max [code, code_unfold, code_inline del]:
"max = ord.max (op \<le>)"
by (rule ext)+ (simp add: max_def ord.max_def)