src/Pure/Thy/term_style.ML
changeset 58011 bc6bced136e5
parent 56204 f70e69208a8c
child 59970 e9f73d87d904
     1.1 --- a/src/Pure/Thy/term_style.ML	Tue Aug 19 18:21:29 2014 +0200
     1.2 +++ b/src/Pure/Thy/term_style.ML	Tue Aug 19 23:17:51 2014 +0200
     1.3 @@ -35,8 +35,8 @@
     1.4  fun parse_single ctxt =
     1.5    Parse.position Parse.xname -- Parse.args >> (fn (name, args) =>
     1.6      let
     1.7 -      val (src, parse) = Args.check_src ctxt (get_data ctxt) (Args.src name args);
     1.8 -      val (f, _) = Args.syntax (Scan.lift parse) src ctxt;
     1.9 +      val (src, parse) = Token.check_src ctxt (get_data ctxt) (Token.src name args);
    1.10 +      val (f, _) = Token.syntax (Scan.lift parse) src ctxt;
    1.11      in f ctxt end);
    1.12  
    1.13  val parse = Args.context :|-- (fn ctxt => Scan.lift