diff -r a5dc3558cdec -r 3b83960f9544 Nominal/Equivp.thy
--- a/Nominal/Equivp.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/Equivp.thy	Thu May 20 21:23:53 2010 +0100
@@ -194,7 +194,7 @@
     else mk_supp ty x
   val lhss = map mk_supp_arg (frees ~~ tys)
   val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
-  val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs)
+  val eq = HOLogic.mk_Trueprop (supports $ fold_union lhss $ rhs)
 in
   (names, eq)
 end
@@ -203,7 +203,7 @@
 ML {*
 fun prove_supports ctxt perms cnst =
 let
-  val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst
+  val (names, eq) = mk_supports_eq ctxt cnst
 in
   Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1)
 end