--- a/src/Pure/simplifier.ML Sun Nov 06 21:17:45 2011 +0100
+++ b/src/Pure/simplifier.ML Sun Nov 06 21:51:46 2011 +0100
@@ -303,7 +303,8 @@
val simproc_att =
(Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) =>
Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt))))
- >> (Library.apply o map Morphism.form);
+ >> (fn atts => Thm.declaration_attribute (fn th =>
+ Library.apply (map (fn att => Thm.attribute_declaration (Morphism.form att) th) atts)));
end;