merged
authorhaftmann
Thu, 11 Mar 2010 09:09:51 +0100
changeset 35709267e15230a31
parent 35707 44936737902d
parent 35708 5e5925871d6f
child 35710 58acd48904bc
merged
     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) =