changeset 36367 | 49c7dee21a7f |
parent 35431 | 8758fe1fc9f8 |
child 37406 | 982f3e02f3c4 |
--- a/src/HOL/Bali/WellType.thy Mon Apr 26 10:57:04 2010 -0700 +++ b/src/HOL/Bali/WellType.thy Mon Apr 26 11:08:49 2010 -0700 @@ -94,7 +94,7 @@ "accObjectmheads G S T \<equiv> if G\<turnstile>RefT T accessible_in (pid S) then Objectmheads G S - else \<lambda>sig. {}" + else (\<lambda>sig. {})" primrec "mheads G S NullT = (\<lambda>sig. {})" "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h))