src/Doc/Eisbach/Manual.thy

--- a/src/Doc/Eisbach/Manual.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Doc/Eisbach/Manual.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -931,7 +931,7 @@
 
     attribute_setup get_split_rule =
       \<open>Args.term >> (fn t =>
-        Thm.rule_attribute (fn context => fn _ =>
+        Thm.rule_attribute [] (fn context => fn _ =>
           (case get_split_rule (Context.proof_of context) t of
             SOME thm => thm
           | NONE => Drule.dummy_thm)))\<close>