src/HOL/BNF/Tools/bnf_comp.ML
changeset 49835 31f32ec4d766
parent 49833 1d80798e8d8a
child 50059 a292751fb345
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Oct 12 18:58:20 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri Oct 12 21:22:35 2012 +0200
     1.3 @@ -625,7 +625,7 @@
     1.4      val deads = map TFree params;
     1.5  
     1.6      val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
     1.7 -      typedef NONE (bdT_bind, params, NoSyn)
     1.8 +      typedef (bdT_bind, params, NoSyn)
     1.9          (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    1.10  
    1.11      val bnf_bd' = mk_dir_image bnf_bd