made SMLNJ happier
authortraytel
Tue Nov 13 12:12:14 2012 +0100 (2012-11-13)
changeset 50059a292751fb345
parent 50058 bb1fadeba35e
child 50060 43753eca324a
made SMLNJ happier
src/HOL/BNF/Tools/bnf_comp.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Tue Nov 13 12:06:43 2012 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Tue Nov 13 12:12:14 2012 +0100
     1.3 @@ -585,7 +585,7 @@
     1.4  
     1.5  (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
     1.6  
     1.7 -fun seal_bnf unfold_set b Ds bnf lthy =
     1.8 +fun seal_bnf (unfold_set : unfold_set) b Ds bnf lthy =
     1.9    let
    1.10      val live = live_of_bnf bnf;
    1.11      val nwits = nwits_of_bnf bnf;