src/Pure/ML/ml_thms.ML
changeset 47815 43f677b3ae91
parent 45592 8baa0b7f3f66
child 48776 37cd53e69840
     1.1 --- a/src/Pure/ML/ml_thms.ML	Fri Apr 27 21:47:47 2012 +0200
     1.2 +++ b/src/Pure/ML/ml_thms.ML	Fri Apr 27 22:47:30 2012 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5            val i = serial ();
     1.6            val srcs = map (Attrib.intern_src thy) raw_srcs;
     1.7 -          val _ = map (Attrib.attribute_i thy) srcs;
     1.8 +          val _ = map (Attrib.attribute background) srcs;
     1.9            val (a, background') = background
    1.10              |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
    1.11            val ml =