diff -r f7be22c6646b -r ab2483fad861 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Mon Aug 25 08:45:32 2014 +0200
+++ b/src/Pure/ML/ml_thms.ML	Mon Aug 25 12:58:20 2014 +0200
@@ -44,10 +44,10 @@
     (fn _ => fn raw_srcs => fn ctxt =>
       let
         val i = serial ();
-        val srcs = map (Attrib.check_src ctxt) raw_srcs;
-        val _ = map (Attrib.attribute ctxt) srcs;
+
         val (a, ctxt') = ctxt
-          |> ML_Antiquotation.variant "attributes" ||> put_attributes (i, srcs);
+          |> ML_Antiquotation.variant "attributes"
+          ||> put_attributes (i, Attrib.check_attribs ctxt raw_srcs);
         val ml =
           ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
             string_of_int i ^ ";\n", "Isabelle." ^ a);