--- a/src/Pure/Isar/object_logic.ML Thu Oct 16 22:44:28 2008 +0200
+++ b/src/Pure/Isar/object_logic.ML Thu Oct 16 22:44:29 2008 +0200
@@ -193,7 +193,7 @@
val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
-val _ = Context.>> (Context.map_theory (add_rulify Drule.norm_hhf_eq));
+val _ = Context.>> (Context.map_theory (fold add_rulify Drule.norm_hhf_eqs));
(* atomize *)