diff -r 77ea2de0ca62 -r 84aef87b348a ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Tue Jul 08 11:34:10 2014 +0100
+++ b/ProgTutorial/Parsing.thy	Wed Aug 20 14:42:14 2014 +0100
@@ -502,7 +502,8 @@
   messages. The following code
 
 
-@{ML_response_fake [display,gray] "Outer_Syntax.scan Position.none \"hello world\"" 
+@{ML_response_fake [display,gray] "Outer_Syntax.scan 
+  (Keyword.get_lexicons ()) Position.none \"hello world\"" 
 "[Token (\<dots>,(Ident, \"hello\"),\<dots>), 
  Token (\<dots>,(Space, \" \"),\<dots>), 
  Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
@@ -520,7 +521,8 @@
 text {*
   then lexing @{text [quotes] "hello world"} will produce
 
-  @{ML_response_fake [display,gray] "Outer_Syntax.scan Position.none \"hello world\"" 
+  @{ML_response_fake [display,gray] "Outer_Syntax.scan 
+  (Keyword.get_lexicons ()) Position.none \"hello world\"" 
 "[Token (\<dots>,(Keyword, \"hello\"),\<dots>), 
  Token (\<dots>,(Space, \" \"),\<dots>), 
  Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
@@ -532,7 +534,7 @@
 
 @{ML_response_fake [display,gray]
 "let
-   val input = Outer_Syntax.scan Position.none \"hello world\"
+   val input = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none \"hello world\"
 in
    filter Token.is_proper input
 end" 
@@ -542,7 +544,7 @@
 *}
 
 ML %grayML{*fun filtered_input str = 
-  filter Token.is_proper (Outer_Syntax.scan Position.none str) *}
+  filter Token.is_proper (Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none str) *}
 
 text {* 
   If you now parse
@@ -669,7 +671,7 @@
 *}
 
 ML %grayML{*fun filtered_input' str = 
-       filter Token.is_proper (Outer_Syntax.scan (Position.line 7) str) *}
+       filter Token.is_proper (Outer_Syntax.scan (Keyword.get_lexicons ()) (Position.line 7) str) *}
 
 text {*
   where we pretend the parsed string starts on line 7. An example is
@@ -758,7 +760,7 @@
 
 @{ML_response_fake [display,gray]
 "let 
-  val input = Outer_Syntax.scan Position.none \"foo\"
+  val input = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none \"foo\"
 in 
   Parse.term input
 end"
@@ -774,7 +776,7 @@
 
 @{ML_response_fake [display,gray]
 "let 
-  val input = Outer_Syntax.scan (Position.line 42) \"foo\"
+  val input = Outer_Syntax.scan (Keyword.get_lexicons ()) (Position.line 42) \"foo\"
 in 
   YXML.parse (fst (Parse.term input))
 end"
@@ -897,7 +899,7 @@
   val input = filtered_input \"foo_lemma[intro,dest!]:\"
   val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input 
 in 
-  (name, map Args.name_of_src attrib)
+  (name, map Token.name_of_src attrib)
 end" "(foo_lemma, [(\"intro\", \<dots>), (\"dest\", \<dots>)])"}
  
   The function @{ML_ind opt_thm_name in Parse_Spec} is the ``optional'' variant of