diff -r f19f4afa49e2 -r d453c69596cc src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Mar 23 23:16:40 2015 +0100
+++ b/src/Tools/Code/code_thingol.ML	Tue Mar 24 11:53:18 2015 +0100
@@ -895,7 +895,7 @@
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
     fun read_const_expr str =
-      (case Syntax.parse_token ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of
+      (case Syntax.parse_input ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of
         SOME "_" => ([], consts_of thy)
       | SOME s =>
           if String.isSuffix "._" s
@@ -910,7 +910,7 @@
   let
     val (consts, consts_permissive) = read_const_exprs_internal ctxt const_exprs;
     val consts' = implemented_deps
-      (consts_program_permissive ((Proof_Context.theory_of ctxt)) consts_permissive);
+      (consts_program_permissive (Proof_Context.theory_of ctxt) consts_permissive);
   in union (op =) consts' consts end;