src/HOL/Tools/legacy_transfer.ML
changeset 61853 fb7756087101
parent 61476 1884c40f1539
child 66795 420d0080545f
--- a/src/HOL/Tools/legacy_transfer.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/legacy_transfer.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -253,7 +253,7 @@
     "install transfer data" #>
     Attrib.setup @{binding transferred}
       (selection -- these (keyword_colon leavingN |-- names)
-        >> (fn (selection, leave) => Thm.rule_attribute (fn context =>
+        >> (fn (selection, leave) => Thm.rule_attribute [] (fn context =>
               Conjunction.intr_balanced o transfer context selection leave)))
     "transfer theorems");