# HG changeset patch
# User haftmann
# Date 1268294991 -3600
# Node ID 267e15230a318936a207af6b3548402abb219e53
# Parent  44936737902dfe4a7d1c7b69ab765ac79f7c6b38# Parent  5e5925871d6f137ea50cecff0f283bbaf00b4248
merged

diff -r 44936737902d -r 267e15230a31 src/HOL/Tools/transfer.ML
--- 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) =