| changeset 6090 | 78c068b838ff |
| parent 6004 | 47705248cf80 |
| child 6113 | b321f5aaa5f4 |
--- a/src/FOL/IFOL.ML Tue Jan 12 13:39:21 1999 +0100 +++ b/src/FOL/IFOL.ML Tue Jan 12 13:39:41 1999 +0100 @@ -441,7 +441,7 @@ local -fun gen_rulify x = Attrib.no_args (Attribute.rule (K (normalize_thm [RSspec, RSmp]))) x; +fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x; in