changeset 61853 | fb7756087101 |
parent 61144 | 5e94dfead1c2 |
child 62913 | 13252110a6fe |
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Dec 15 16:57:10 2015 +0100 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Dec 16 16:31:36 2015 +0100 @@ -755,7 +755,7 @@ (* lifting as an attribute *) -val lifted_attrib = Thm.rule_attribute (fn context => +val lifted_attrib = Thm.rule_attribute [] (fn context => let val ctxt = Context.proof_of context val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)