--- 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;