src/HOL/UNITY/Comp/Alloc.thy

       handle THM _ => th RS @{thm lessThanBspec}
       handle THM _ => th RS bspec
       handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
     handle THM _ => th;
 in
-  Scan.succeed (Thm.rule_attribute (K normalized))
+  Scan.succeed (Thm.rule_attribute [] (K normalized))
 end
 *}
 
 (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
 ML {*