src/HOL/Bali/Conform.thy
changeset 30235 58d147683393
parent 24783 5a3e336a2e37
child 32960 69916a850301
--- a/src/HOL/Bali/Conform.thy	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Bali/Conform.thy	Wed Mar 04 10:47:20 2009 +0100
@@ -102,7 +102,7 @@
 constdefs
 
   conf  :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool"    ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
-	   "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. option_map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T"
+	   "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. Option.map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T"
 
 lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
 by (auto simp: conf_def)