diff -r 568840962230 -r bc6bced136e5 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/recdef.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -15,17 +15,17 @@
   val cong_del: attribute
   val wf_add: attribute
   val wf_del: attribute
-  val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
-    Attrib.src option -> theory -> theory
+  val add_recdef: bool -> xstring -> string -> ((binding * string) * Token.src list) list ->
+    Token.src option -> theory -> theory
       * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
     theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
-  val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
+  val defer_recdef: xstring -> string list -> (Facts.ref * Token.src list) list
     -> theory -> theory * {induct_rules: thm}
   val defer_recdef_i: xstring -> term list -> thm list -> theory -> theory * {induct_rules: thm}
-  val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> bool ->
+  val recdef_tc: bstring * Token.src list -> xstring -> int option -> bool ->
     local_theory -> Proof.state
-  val recdef_tc_i: bstring * Attrib.src list -> string -> int option -> bool ->
+  val recdef_tc_i: bstring * Token.src list -> string -> int option -> bool ->
     local_theory -> Proof.state
   val setup: theory -> theory
 end;
@@ -164,7 +164,7 @@
     val ctxt =
       (case opt_src of
         NONE => ctxt0
-      | SOME src => #2 (Args.syntax (Method.sections recdef_modifiers) src ctxt0));
+      | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt0));
     val {simps, congs, wfs} = get_hints ctxt;
     val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
   in (ctxt', rev (map snd congs), wfs) end;
@@ -292,7 +292,7 @@
 val hints =
   @{keyword "("} |--
     Parse.!!! (Parse.position @{keyword "hints"} -- Parse.args --| @{keyword ")"})
-  >> uncurry Args.src;
+  >> uncurry Token.src;
 
 val recdef_decl =
   Scan.optional