# HG changeset patch
# User traytel
# Date 1352805134 -3600
# Node ID a292751fb3453549ece577ac5d9343778824e882
# Parent  bb1fadeba35e3993540fd2833603c4c17fcea89c
made SMLNJ happier

diff -r bb1fadeba35e -r a292751fb345 src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Tue Nov 13 12:06:43 2012 +0100
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Tue Nov 13 12:12:14 2012 +0100
@@ -585,7 +585,7 @@
 
 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
 
-fun seal_bnf unfold_set b Ds bnf lthy =
+fun seal_bnf (unfold_set : unfold_set) b Ds bnf lthy =
   let
     val live = live_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;