author | haftmann |
Thu, 11 Mar 2010 09:09:43 +0100 | |
changeset 35708 | 5e5925871d6f |
parent 35691 | d9c9b81b16a8 |
child 35709 | 267e15230a31 |
--- a/src/HOL/Tools/transfer.ML Wed Mar 10 15:29:23 2010 +0100 +++ b/src/HOL/Tools/transfer.ML Thu Mar 11 09:09:43 2010 +0100 @@ -51,7 +51,7 @@ (* data lookup *) -fun transfer_rules_of { inj, embed, return, cong, ... } = +fun transfer_rules_of ({ inj, embed, return, cong, ... } : entry) = (inj, embed, return, cong); fun get_by_direction context (a, D) =