diff -r b84688dd7f6b -r 1ca1142e1711 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Wed Dec 09 16:22:29 2015 +0100
+++ b/src/Pure/ML/ml_thms.ML	Wed Dec 09 16:36:26 2015 +0100
@@ -40,11 +40,11 @@
 (* attribute source *)
 
 val _ = Theory.setup
-  (ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse.attribs)
-    (fn _ => fn raw_srcs => fn ctxt =>
+  (ML_Antiquotation.declaration @{binding attributes} Attrib.attribs
+    (fn _ => fn srcs => fn ctxt =>
       let val i = serial () in
         ctxt
-        |> put_attributes (i, Attrib.check_attribs ctxt raw_srcs)
+        |> put_attributes (i, srcs)
         |> ML_Context.value_decl "attributes"
             ("ML_Thms.the_attributes ML_context " ^ string_of_int i)
       end));