--- a/src/HOL/Nominal/nominal_datatype.ML Wed Jul 22 14:20:31 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Jul 22 14:20:32 2009 +0200
@@ -1013,7 +1013,7 @@
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(supp c,
if null dts then HOLogic.mk_set atomT []
- else foldr1 (HOLogic.mk_binop @{const_name Un}) (map supp args2)))))
+ else foldr1 (HOLogic.mk_binop @{const_name union}) (map supp args2)))))
(fn _ =>
simp_tac (HOL_basic_ss addsimps (supp_def ::
Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::