src/Pure/Tools/rule_insts.ML

     -- Parse.for_fixes;
 
 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");
 
 
 (* of: positional instantiation (terms only) *)
 

 in
 
 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;