src/Pure/System/session.scala
changeset 36947 285b39022372
parent 36782 0499d05663dd
child 37041 dae419819a80
     1.1 --- a/src/Pure/System/session.scala	Sat May 15 21:57:27 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sat May 15 22:05:49 2010 +0200
     1.3 @@ -140,8 +140,8 @@
     1.4              }
     1.5  
     1.6            // keyword declarations
     1.7 -          case List(Outer_Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
     1.8 -          case List(Outer_Keyword.Keyword_Decl(name)) => syntax += name
     1.9 +          case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    1.10 +          case List(Keyword.Keyword_Decl(name)) => syntax += name
    1.11  
    1.12            case _ => if (!result.is_ready) bad_result(result)
    1.13          }