--- a/src/HOL/MicroJava/J/Conform.thy Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Fri Feb 14 07:53:46 2014 +0100
@@ -14,7 +14,7 @@
definition conf :: "'c prog => aheap => val => ty => bool"
("_,_ |- _ ::<= _" [51,51,51,51] 50) where
- "G,h|-v::<=T == \<exists>T'. typeof (Option.map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
+ "G,h|-v::<=T == \<exists>T'. typeof (map_option obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
definition lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
("_,_ |- _ [::<=] _" [51,51,51,51] 50) where