merged
authorhaftmann
Thu, 11 Mar 2010 09:09:51 +0100
changeset 35709 267e15230a31
parent 35707 44936737902d (current diff)
parent 35708 5e5925871d6f (diff)
child 35710 58acd48904bc
merged
--- a/src/HOL/Tools/transfer.ML	Wed Mar 10 16:06:48 2010 -0800
+++ b/src/HOL/Tools/transfer.ML	Thu Mar 11 09:09:51 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) =