diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/term.scala --- a/src/Pure/term.scala Tue Jul 12 16:00:05 2011 +0900 +++ b/src/Pure/term.scala Tue Jul 12 10:44:30 2011 +0200 @@ -43,7 +43,7 @@ object Encode { - import XML_Data.Encode._ + import XML.Encode._ val indexname: T[Indexname] = pair(string, int) @@ -67,7 +67,7 @@ object Decode { - import XML_Data.Decode._ + import XML.Decode._ val indexname: T[Indexname] = pair(string, int)