diff -r 32979078bfe9 -r d2154b421707 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Tue May 31 00:17:22 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Tue May 31 00:36:16 2011 +0100
@@ -123,28 +123,26 @@
     |> HOLogic.mk_Trueprop
   end
 
-fun mk_eqvt_proof_obligation qs fvar (assms, arg) = 
+(** building proof obligations *)
+fun mk_eqvt_proof_obligation qs fvar (_, assms, arg) = 
   mk_eqvt_at (fvar, arg)
-  |> curry Logic.list_implies assms
+  |> curry Logic.list_implies (map prop_of assms)
   |> curry Term.list_abs_free qs
   |> strip_abs_body
 
 (** building proof obligations *)
-
-fun mk_compat_proof_obligations lthy domT ranT fvar f RCss glrs =
+fun mk_compat_proof_obligations domT ranT fvar f RCss glrs =
   let
     fun mk_impl (((qs, gs, lhs, rhs), RCs), ((qs', gs', lhs', rhs'), _)) =
       let
         val shift = incr_boundvars (length qs')
-     
-        val rc_args = map (fn (_, thms, args) => (map prop_of thms, args)) RCs
-        val tt = map (shift o mk_eqvt_proof_obligation qs fvar) rc_args
+        val eqvts_proof_obligations = map (shift o mk_eqvt_proof_obligation qs fvar) RCs
       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) tt (* nominal *)
+        |> fold_rev (curry Logic.mk_implies) eqvts_proof_obligations (* 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
@@ -958,7 +956,7 @@
       mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
 
     val compat =
-      mk_compat_proof_obligations lthy domT ranT fvar f RCss abstract_qglrs 
+      mk_compat_proof_obligations domT ranT fvar f RCss abstract_qglrs 
       |> map (cert #> Thm.assume)
 
     val G_eqvt = mk_eqvt G |> cert |> Thm.assume