# HG changeset patch
# User haftmann
# Date 1268294983 -3600
# Node ID 5e5925871d6f137ea50cecff0f283bbaf00b4248
# Parent  d9c9b81b16a80221c271fbae795b2e10b41ac3f5
made smlnj happy

diff -r d9c9b81b16a8 -r 5e5925871d6f src/HOL/Tools/transfer.ML
--- 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) =