author | haftmann |
Thu, 11 Mar 2010 09:09:51 +0100 | |
changeset 35709 | 267e15230a31 |
parent 35707 | 44936737902d |
parent 35708 | 5e5925871d6f |
child 35710 | 58acd48904bc |
1.1 --- a/src/HOL/Tools/transfer.ML Wed Mar 10 16:06:48 2010 -0800 1.2 +++ b/src/HOL/Tools/transfer.ML Thu Mar 11 09:09:51 2010 +0100 1.3 @@ -51,7 +51,7 @@ 1.4 1.5 (* data lookup *) 1.6 1.7 -fun transfer_rules_of { inj, embed, return, cong, ... } = 1.8 +fun transfer_rules_of ({ inj, embed, return, cong, ... } : entry) = 1.9 (inj, embed, return, cong); 1.10 1.11 fun get_by_direction context (a, D) =