changeset 49833 | 1d80798e8d8a |
parent 49714 | 2c7c32f34220 |
child 49835 | 31f32ec4d766 |
--- a/src/HOL/BNF/Tools/bnf_comp.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Fri Oct 12 15:08:29 2012 +0200 @@ -625,7 +625,7 @@ val deads = map TFree params; val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) = - typedef false NONE (bdT_bind, params, NoSyn) + typedef NONE (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val bnf_bd' = mk_dir_image bnf_bd