fix another if-then-else parse error
authorhuffman
Mon Apr 26 11:08:49 2010 -0700 (2010-04-26)
changeset 3636749c7dee21a7f
parent 36366 886b94b1bed7
child 36368 1b5b9bbab006
child 36403 9a4baad039c4
child 36431 340755027840
fix another if-then-else parse error
src/HOL/Bali/WellType.thy
     1.1 --- a/src/HOL/Bali/WellType.thy	Mon Apr 26 10:57:04 2010 -0700
     1.2 +++ b/src/HOL/Bali/WellType.thy	Mon Apr 26 11:08:49 2010 -0700
     1.3 @@ -94,7 +94,7 @@
     1.4  "accObjectmheads G S T
     1.5     \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
     1.6          then Objectmheads G S
     1.7 -        else \<lambda>sig. {}"
     1.8 +        else (\<lambda>sig. {})"
     1.9  primrec
    1.10  "mheads G S  NullT     = (\<lambda>sig. {})"
    1.11  "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h))