src/Pure/Isar/attrib.ML
changeset 30211 556d1810cdad
parent 30190 479806475f3c
child 30242 aea5d7fa7ef5
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Mar 03 14:07:23 2009 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Mar 03 14:07:43 2009 +0100
     1.3 @@ -118,8 +118,7 @@
     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 -    [((Binding.empty, []),
     1.8 -      map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
     1.9 +    [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
    1.10    |> fst |> maps snd;
    1.11  
    1.12