diff -r 79136ce06bdb -r 58d147683393 src/HOL/NanoJava/State.thy
--- a/src/HOL/NanoJava/State.thy	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/NanoJava/State.thy	Wed Mar 04 10:47:20 2009 +0100
@@ -33,7 +33,7 @@
 constdefs
 
   init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)"
- "init_vars m == option_map (\<lambda>T. Null) o m"
+ "init_vars m == Option.map (\<lambda>T. Null) o m"
   
 text {* private: *}
 types	heap   = "loc   \<rightharpoonup> obj"