src/Pure/Tools/rule_insts.ML

--- a/src/Pure/Tools/rule_insts.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -182,7 +182,7 @@
 val _ = Theory.setup
   (Attrib.setup @{binding "where"}
     (Scan.lift named_insts >> (fn args =>
-      Thm.rule_attribute (fn context => uncurry (where_rule (Context.proof_of context)) args)))
+      Thm.rule_attribute [] (fn context => uncurry (where_rule (Context.proof_of context)) args)))
     "named instantiation of theorem");
 
 
@@ -202,7 +202,7 @@
 val _ = Theory.setup
   (Attrib.setup @{binding "of"}
     (Scan.lift (insts -- Parse.for_fixes) >> (fn args =>
-      Thm.rule_attribute (fn context => uncurry (of_rule (Context.proof_of context)) args)))
+      Thm.rule_attribute [] (fn context => uncurry (of_rule (Context.proof_of context)) args)))
     "positional instantiation of theorem");
 
 end;