src/Tools/Code/code_thingol.ML

       ((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
     fun belongs_here thy' c = forall
       (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) Markup.empty (SOME o Symbol_Pos.implode o #1) str of
+      (case Syntax.parse_token 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
           then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s)))
           else ([Code.read_const thy str], [])