diff -r d273c24b5776 -r fb7756087101 src/HOL/Tools/legacy_transfer.ML --- 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");