src/HOL/UNITY/Comp/Alloc.thy

--- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -321,7 +321,7 @@
       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
 *}