--- a/src/Tools/Code/code_target.ML Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Tools/Code/code_target.ML Wed Dec 03 14:04:38 2014 +0100
@@ -696,7 +696,7 @@
val thy = Thy_Info.get_theory thyname;
val ctxt = Proof_Context.init_global thy;
val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
- (filter Token.is_proper o Outer_Syntax.scan (Thy_Header.get_keywords thy) Position.none);
+ (filter Token.is_proper o Token.explode (Thy_Header.get_keywords thy) Position.none);
in case parse cmd_expr
of SOME f => (writeln "Now generating code..."; f ctxt)
| NONE => error ("Bad directive " ^ quote cmd_expr)