src/Pure/Thy/term_style.ML

--- a/src/Pure/Thy/term_style.ML	Wed Dec 09 16:22:29 2015 +0100
+++ b/src/Pure/Thy/term_style.ML	Wed Dec 09 16:36:26 2015 +0100
@@ -24,7 +24,6 @@
 );
 
 val get_data = Data.get o Proof_Context.theory_of;
-val get_style = Name_Space.get o get_data;
 
 fun setup binding style thy =
   Data.map (#2 o Name_Space.define (Context.Theory thy) true (binding, style)) thy;
@@ -33,9 +32,9 @@
 (* style parsing *)
 
 fun parse_single ctxt =
-  Parse.position Parse.xname -- Parse.args >> (fn (name, args) =>
+  Parse.token Parse.xname ::: Parse.args >> (fn src0 =>
     let
-      val (src, parse) = Token.check_src ctxt (get_data ctxt) (Token.src name args);
+      val (src, parse) = Token.check_src ctxt get_data src0;
       val (f, _) = Token.syntax (Scan.lift parse) src ctxt;
     in f ctxt end);