changeset 30235 | 58d147683393 |
parent 16417 | 9bc16273c2d4 |
child 35102 | cc7a0b9f938c |
--- a/src/HOL/MicroJava/J/Exceptions.thy Tue Mar 03 17:05:18 2009 +0100 +++ b/src/HOL/MicroJava/J/Exceptions.thy Wed Mar 04 10:47:20 2009 +0100 @@ -21,7 +21,7 @@ cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname" translations - "cname_of hp v" == "fst (the (hp (the_Addr v)))" + "cname_of hp v" == "fst (CONST the (hp (the_Addr v)))" constdefs