src/Pure/Isar/method.ML
changeset 45375 7fe19930dfc9
parent 45228 aa3ad19c05d5
child 46466 61c7214b4885
--- a/src/Pure/Isar/method.ML	Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Pure/Isar/method.ML	Sun Nov 06 21:51:46 2011 +0100
@@ -396,7 +396,8 @@
 local
 
 fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
-fun app (f, att) (context, ths) = Library.foldl_map att (Context.map_proof f context, ths);
+fun app (f, att) (context, ths) =
+  Library.foldl_map (Thm.apply_attribute att) (Context.map_proof f context, ths);
 
 in