diff -r 25a7f421a3ba -r 47063163f333 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Thu Jun 16 12:12:25 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Thu Jun 16 13:14:16 2011 +0100
@@ -157,18 +157,22 @@
 (** building proof obligations *)
 fun mk_compat_proof_obligations domT ranT fvar f RCss inv glrs =
   let
-    fun mk_impl (((qs, gs, lhs, rhs), RCs), ((qs', gs', lhs', rhs'), _)) =
+    fun mk_impl (((qs, gs, lhs, rhs), RCs_lhs), ((qs', gs', lhs', rhs'), RCs_rhs)) =
       let
         val shift = incr_boundvars (length qs')
-        val eqvts_proof_obligations = map (shift o mk_eqvt_proof_obligation qs fvar) RCs
-        val invs_proof_obligations = map (shift o mk_inv_proof_obligation inv qs fvar) RCs
+        val eqvts_obligations_lhs = map (shift o mk_eqvt_proof_obligation qs fvar) RCs_lhs
+        val eqvts_obligations_rhs = map (mk_eqvt_proof_obligation qs' fvar) RCs_rhs
+        val invs_obligations_lhs = map (shift o mk_inv_proof_obligation inv qs fvar) RCs_lhs
+        val invs_obligations_rhs = map (mk_inv_proof_obligation inv qs' fvar) RCs_rhs
       in
         Logic.mk_implies
           (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
             HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
         |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
-        |> fold_rev (curry Logic.mk_implies) invs_proof_obligations (* nominal *)
-        |> fold_rev (curry Logic.mk_implies) eqvts_proof_obligations (* nominal *)
+        |> fold_rev (curry Logic.mk_implies) invs_obligations_rhs (* nominal *)
+        |> fold_rev (curry Logic.mk_implies) invs_obligations_lhs (* nominal *)
+        |> fold_rev (curry Logic.mk_implies) eqvts_obligations_rhs (* nominal *)
+        |> fold_rev (curry Logic.mk_implies) eqvts_obligations_lhs (* nominal *)
         |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
         |> curry abstract_over fvar
         |> curry subst_bound f
@@ -298,7 +302,9 @@
       compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
       |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
       |> fold Thm.elim_implies eqvtsj (* nominal *)
+      |> fold Thm.elim_implies eqvtsi (* nominal *)
       |> fold Thm.elim_implies invsj (* nominal *)
+      |> fold Thm.elim_implies invsi (* nominal *)
       |> fold Thm.elim_implies agsj
       |> fold Thm.elim_implies agsi
       |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
@@ -310,7 +316,9 @@
       compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
       |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
       |> fold Thm.elim_implies eqvtsi  (* nominal *)
+      |> fold Thm.elim_implies eqvtsj  (* nominal *)
       |> fold Thm.elim_implies invsi  (* nominal *)
+      |> fold Thm.elim_implies invsj  (* nominal *)
       |> fold Thm.elim_implies agsi
       |> fold Thm.elim_implies agsj
       |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)