replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed

--- a/src/HOL/Divides.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/Divides.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -131,7 +131,7 @@
   note that ultimately show thesis by blast
 qed
 
-lemma dvd_eq_mod_eq_0 [code, code_unfold, code_inline del]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
 proof
   assume "b mod a = 0"
   with mod_div_equality [of b a] have "b div a * a = b" by simp

--- a/src/HOL/HOL.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/HOL.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -1729,7 +1729,7 @@
   assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
 begin
 
-lemma equal [code_unfold, code_inline del]: "equal = (op =)"
+lemma equal: "equal = (op =)"
   by (rule ext equal_eq)+
 
 lemma equal_refl: "equal x x \<longleftrightarrow> True"

--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -495,7 +495,7 @@
 lemma [code_post]: "raise' (STR s) = raise s"
 unfolding raise'_def by (simp add: STR_inverse)
 
-lemma raise_raise' [code_inline]:
+lemma raise_raise' [code_unfold]:
   "raise s = raise' (STR s)"
   unfolding raise'_def by (simp add: STR_inverse)
 

--- a/src/HOL/Library/Executable_Set.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -67,7 +67,7 @@
   "{} = empty"
   by simp
 
-lemma [code_unfold, code_inline del]:
+lemma
   "empty = Set []"
   by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}
 

--- a/src/HOL/Library/Mapping.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/Library/Mapping.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -90,7 +90,7 @@
 
 subsection {* Properties *}
 
-lemma keys_is_none_lookup [code_inline]:
+lemma keys_is_none_lookup [code_unfold]:
   "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
   by (auto simp add: keys_def is_none_def)
 

--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -84,7 +84,7 @@
 
 definition subtract
 where
-  [code_inline]: "subtract x y = y - x"
+  [code_unfold]: "subtract x y = y - x"
 
 setup {*
 let

--- a/src/HOL/Library/Transitive_Closure_Table.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -185,8 +185,6 @@
     by (auto simp add: rtranclp_eq_rtrancl_path)
 qed
 
-declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
-
 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
 
 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce

--- a/src/HOL/MicroJava/J/JListExample.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -118,12 +118,12 @@
 
 definition undefined_cname :: cname 
   where [code del]: "undefined_cname = undefined"
-declare undefined_cname_def[symmetric, code_inline]
+declare undefined_cname_def[symmetric, code_unfold]
 code_datatype Object Xcpt Cname undefined_cname
 
 definition undefined_val :: val
   where [code del]: "undefined_val = undefined"
-declare undefined_val_def[symmetric, code_inline]
+declare undefined_val_def[symmetric, code_unfold]
 code_datatype Unit Null Bool Intg Addr undefined_val
 
 definition E where 

--- a/src/HOL/MicroJava/J/SystemClasses.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/MicroJava/J/SystemClasses.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -13,18 +13,18 @@
 *}
 
 definition ObjectC :: "'c cdecl" where
-  [code_inline]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
+  [code_unfold]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
 
 definition NullPointerC :: "'c cdecl" where
-  [code_inline]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
+  [code_unfold]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
 
 definition ClassCastC :: "'c cdecl" where
-  [code_inline]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
+  [code_unfold]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
 
 definition OutOfMemoryC :: "'c cdecl" where
-  [code_inline]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
+  [code_unfold]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
 
 definition SystemClasses :: "'c cdecl list" where
-  [code_inline]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
+  [code_unfold]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
 
 end

--- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -97,7 +97,7 @@
   [inductify]
   subcls'
 .
-lemma subcls_conv_subcls' [code_inline]:
+lemma subcls_conv_subcls' [code_unfold]:
   "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
 by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
 

--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -125,11 +125,11 @@
 definition undefined_cname :: cname 
   where [code del]: "undefined_cname = undefined"
 code_datatype Object Xcpt Cname undefined_cname
-declare undefined_cname_def[symmetric, code_inline]
+declare undefined_cname_def[symmetric, code_unfold]
 
 definition undefined_val :: val
   where [code del]: "undefined_val = undefined"
-declare undefined_val_def[symmetric, code_inline]
+declare undefined_val_def[symmetric, code_unfold]
 code_datatype Unit Null Bool Intg Addr undefined_val
 
 definition

--- a/src/HOL/Nat.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/Nat.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -1301,7 +1301,7 @@
 
 end
 
-declare of_nat_code [code, code_unfold, code_inline del]
+declare of_nat_code [code]
 
 text{*Class for unital semirings with characteristic zero.
  Includes non-ordered rings like the complex numbers.*}

--- 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)
 

--- a/src/HOL/Power.thy	Fri Oct 21 11:17:12 2011 +0200
+++ b/src/HOL/Power.thy	Fri Oct 21 11:17:14 2011 +0200
@@ -460,7 +460,7 @@
 
 subsection {* Code generator tweak *}
 
-lemma power_power_power [code, code_unfold, code_inline del]:
+lemma power_power_power [code]:
   "power = power.power (1::'a::{power}) (op *)"
   unfolding power_def power.power_def ..