src/Pure/Isar/attrib.ML
changeset 28083 103d9282a946
parent 27865 27a8ad9612a3
child 28084 a05ca48ef263
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -110,7 +110,8 @@
     1.4  fun attribute thy = attribute_i thy o intern_src thy;
     1.5  
     1.6  fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
     1.7 -    [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
     1.8 +    [((Name.no_binding, []),
     1.9 +      map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
    1.10    |> fst |> maps snd;
    1.11  
    1.12