changeset 30450 | 7655e6533209 |
parent 30364 | 577edc39b501 |
child 31458 | b1cf26f2919b |
--- a/src/HOL/Nominal/nominal_package.ML Wed Mar 11 15:56:50 2009 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Wed Mar 11 15:56:51 2009 +0100 @@ -1011,7 +1011,7 @@ (augment_sort thy8 pt_cp_sort (HOLogic.mk_Trueprop (HOLogic.mk_eq (supp c, - if null dts then Const (@{const_name Set.empty}, HOLogic.mk_setT atomT) + if null dts then HOLogic.mk_set atomT [] else foldr1 (HOLogic.mk_binop @{const_name Un}) (map supp args2))))) (fn _ => simp_tac (HOL_basic_ss addsimps (supp_def ::