diff -r 5ecb857e9de7 -r 3b9ef98a03d2 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Wed Jun 01 16:13:42 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Wed Jun 01 21:03:30 2011 +0100
@@ -124,8 +124,9 @@
   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 Term.list_all_free vs
   |> curry Logic.list_implies (map prop_of assms)
   |> curry Term.list_abs_free qs
   |> strip_abs_body
@@ -265,12 +266,16 @@
     val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj
 
     val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
+
+    val _ = tracing ("eqvtsi\n" ^ cat_lines (map (Syntax.string_of_term_global thy o prop_of) eqvtsi))
+    val _ = tracing ("eqvtsj\n" ^ cat_lines (map (Syntax.string_of_term_global thy o prop_of) eqvtsj))
   in if j < i then
     let
       val compat = lookup_compat_thm j i cts
     in
       compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
       |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
+      |> tap (fn t => tracing ("1: " ^ Syntax.string_of_term_global thy (prop_of t)))
       |> fold Thm.elim_implies eqvtsj (* nominal *)
       |> fold Thm.elim_implies agsj
       |> fold Thm.elim_implies agsi
@@ -282,6 +287,7 @@
     in
       compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
       |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
+      |> tap (fn t => tracing ("2: " ^ Syntax.string_of_term_global thy (prop_of t)))
       |> fold Thm.elim_implies eqvtsi  (* nominal *)
       |> fold Thm.elim_implies agsi
       |> fold Thm.elim_implies agsj
@@ -336,7 +342,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)