--- a/Nominal/nominal_dt_quot.ML	Mon Jan 03 16:21:12 2011 +0000
+++ b/Nominal/nominal_dt_quot.ML	Tue Jan 04 13:47:38 2011 +0000
@@ -466,7 +466,7 @@
       |> mk_perm (Bound 0)
 
     val goal = mk_fresh_star lhs rhs
-      |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t))
+      |> mk_exists ("p", @{typ perm})
       |> HOLogic.mk_Trueprop   
  
     val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp}