# HG changeset patch
# User wenzelm
# Date 1398441294 -7200
# Node ID ba1ac087b3a771b1cf35959ae36511b299baef54
# Parent  f2ffead641d46c027dd50bb85ab2874affc5a328
make SML/NJ happier;

diff -r f2ffead641d4 -r ba1ac087b3a7 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Fri Apr 25 14:39:11 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Fri Apr 25 17:54:54 2014 +0200
@@ -55,7 +55,7 @@
 
 type pred_data = {rel_eq_onp: thm}
 
-val rel_eq_onp = #rel_eq_onp
+val rel_eq_onp: pred_data -> thm = #rel_eq_onp
 
 structure Data = Generic_Data
 (