made SMLNJ happier
authortraytel
Tue, 13 Nov 2012 12:12:14 +0100
changeset 50059 a292751fb345
parent 50058 bb1fadeba35e
child 50060 43753eca324a
made SMLNJ happier
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;