src/HOL/MicroJava/JVM/JVMListExample.thy

--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Oct 31 09:28:56 2006 +0100
@@ -113,7 +113,7 @@
   "next_nam" ("\"next\"")
 
 code_type cnam and vnam and mname and loc_
-  (SML target_atom "string" and target_atom "string" and target_atom "string" and target_atom "IntInf.int")
+  (SML "string" and "string" and "string" and "IntInf.int")
 
 instance cnam :: eq
   and cname :: eq
@@ -138,15 +138,15 @@
   arbitrary_cname \<equiv> object'
 
 code_const list_nam and test_nam and append_name and makelist_name and val_nam and next_nam
-  (SML target_atom "\"list\"" and target_atom "\"test\"" and target_atom "\"append\""
-    and target_atom "\"makelist\"" and target_atom "\"val\"" and target_atom "\"next\"")
+  (SML "\"list\"" and "\"test\"" and "\"append\""
+    and "\"makelist\"" and "\"val\"" and "\"next\"")
 
 axiomatization
   incr_loc :: "loc_ \<Rightarrow> loc_"
   and zero_loc :: "loc_"
 
 code_const incr_loc and zero_loc
-  (SML target_atom "(_ + 1)" and target_atom "0")
+  (SML "(op +)/ (_, 1)" and "0")
 
 axiomatization
   test_loc :: "(loc_ \<Rightarrow> bool) \<Rightarrow> (loc_ \<Rightarrow> 'a) \<Rightarrow> loc_ \<Rightarrow> 'a" where
@@ -155,13 +155,13 @@
 definition
   new_addr' :: "(loc \<Rightarrow> (cname \<times> (vname \<times> cname \<Rightarrow> val option)) option) \<Rightarrow> loc \<times> val option"
   "new_addr' hp =
-    test_loc (\<lambda>i. is_none (hp (Loc i) )) (\<lambda>i. (Loc i, None)) zero_loc"
+    test_loc (\<lambda>i. hp (Loc i) = None) (\<lambda>i. (Loc i, None)) zero_loc"
 
 lemma [code func]:
   "wf_class = wf_class" ..
 
 code_const
-  wf_class (SML target_atom "(fn _ => true)")
+  wf_class (SML "(fn `_ => true)")
 
 code_axioms
   new_Addr \<equiv> new_addr'