--- a/src/HOL/Orderings.thy Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/Orderings.thy Fri Oct 21 11:17:14 2011 +0200
@@ -305,13 +305,13 @@
text {* Explicit dictionaries for code generation *}
-lemma min_ord_min [code, code_unfold, code_inline del]:
+lemma min_ord_min [code]:
"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]:
"max = ord.max (op \<le>)"
by (rule ext)+ (simp add: max_def ord.max_def)