diff -r 4cd1a7e7edac -r 0fdf5708c7a8 src/HOL/NanoJava/State.thy
--- a/src/HOL/NanoJava/State.thy	Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/NanoJava/State.thy	Fri Jul 25 17:21:22 2003 +0200
@@ -21,7 +21,7 @@
   | Addr loc    --{* address, i.e. location of object *}
 
 types	fields
-	= "(fname \<leadsto> val)"
+	= "(fname \<rightharpoonup> val)"
 
         obj = "cname \<times> fields"
 
@@ -32,12 +32,12 @@
 
 constdefs
 
-  init_vars:: "('a \<leadsto> 'b) => ('a \<leadsto> val)"
+  init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)"
  "init_vars m == option_map (\<lambda>T. Null) o m"
   
 text {* private: *}
-types	heap   = "loc   \<leadsto> obj"
-        locals = "vname \<leadsto> val"	
+types	heap   = "loc   \<rightharpoonup> obj"
+        locals = "vname \<rightharpoonup> val"	
 
 text {* private: *}
 record  state