author | huffman |
Mon, 26 Apr 2010 11:08:49 -0700 | |
changeset 36367 | 49c7dee21a7f |
parent 36366 | 886b94b1bed7 |
child 36368 | 1b5b9bbab006 |
child 36403 | 9a4baad039c4 |
child 36431 | 340755027840 |
--- 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))