diff -r 77ea2de0ca62 -r 84aef87b348a ProgTutorial/Package/Ind_Interface.thy --- a/ProgTutorial/Package/Ind_Interface.thy Tue Jul 08 11:34:10 2014 +0100 +++ b/ProgTutorial/Package/Ind_Interface.thy Wed Aug 20 14:42:14 2014 +0100 @@ -96,7 +96,7 @@ where accpartI: "(\y. R y x \ accpart' y) \ accpart' x" (*<*)ML %no{*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) fun parse p input = Scan.finite Token.stopper (Scan.error p) input*}(*>*) text {* Note that in these definitions the parameter @{text R}, standing for the