src/HOL/BNF/Tools/bnf_comp.ML
changeset 50059 a292751fb345
parent 49835 31f32ec4d766
child 51551 88d1d19fb74f
     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;