# HG changeset patch
# User huffman
# Date 1272305329 25200
# Node ID 49c7dee21a7f3344b28446452a2cee9bbb3f548a
# Parent  886b94b1bed7ce9c8ecaaa04191bb1fe47fa5844
fix another if-then-else parse error

diff -r 886b94b1bed7 -r 49c7dee21a7f src/HOL/Bali/WellType.thy
--- 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))