diff -r db0ed02eba6e -r a72a04f3d6bf Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Thu Jun 02 10:09:23 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Thu Jun 02 10:11:50 2011 +0900
@@ -124,9 +124,10 @@
   end
 
 (** building proof obligations *)
-fun mk_eqvt_proof_obligation qs fvar (_, assms, arg) = 
+fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = 
   mk_eqvt_at (fvar, arg)
   |> curry Logic.list_implies (map prop_of assms)
+  |> curry Term.list_all_free vs
   |> curry Term.list_abs_free qs
   |> strip_abs_body
 
@@ -336,7 +337,7 @@
     fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = 
         (llRI RS ih_eqvt_case)
         |> fold_rev (Thm.implies_intr o cprop_of) CCas
-        (* fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs *)
+        |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs 
   in
     map prep_eqvt RCs
     |> map (fold_rev (Thm.implies_intr o cprop_of) ags)