diff -r ee139d9d7ab8 -r abe5306cacbe ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Wed Jul 22 13:59:37 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Wed Jul 22 14:02:47 2009 +0200
@@ -624,7 +624,7 @@
 
 text {*
   There is usually no need to write your own parser for parsing inner syntax, that is 
-  for terms and  types: you can just call the pre-defined parsers. Terms can 
+  for terms and  types: you can just call the predefined parsers. Terms can 
   be parsed using the function @{ML OuterParse.term}. For example:
 
 @{ML_response [display,gray]