--- a/Nominal/nominal_function_core.ML	Thu May 26 06:36:29 2011 +0200
+++ b/Nominal/nominal_function_core.ML	Tue May 31 00:17:22 2011 +0100
@@ -123,39 +123,34 @@
     |> HOLogic.mk_Trueprop
   end
 
-(* nominal *)
-fun find_calls2 f t = 
-  let
-    fun aux (g $ arg) = aux g #> aux arg #> (if f = g then cons ((g, arg)) else I)
-      | aux (Abs (_, _, t)) = aux t 
-      | aux _ = I
-  in
-    aux t []
-  end 
-
-
+fun mk_eqvt_proof_obligation qs fvar (assms, arg) = 
+  mk_eqvt_at (fvar, arg)
+  |> curry Logic.list_implies assms
+  |> curry Term.list_abs_free qs
+  |> strip_abs_body
 
 (** building proof obligations *)
 
-fun mk_compat_proof_obligations domT ranT fvar f glrs =
+fun mk_compat_proof_obligations lthy domT ranT fvar f RCss glrs =
   let
-    fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) =
+    fun mk_impl (((qs, gs, lhs, rhs), RCs), ((qs', gs', lhs', rhs'), _)) =
       let
         val shift = incr_boundvars (length qs')
-
-        val RCs_rhs  = find_calls2 fvar rhs (* nominal : FIXME : recursive calls should be passed here *)
+     
+        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
       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) (map (shift o mk_eqvt_at) RCs_rhs) (* nominal *)
+        |> fold_rev (curry Logic.mk_implies) tt (* 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
       end
   in
-    map mk_impl (unordered_pairs glrs)
+    map mk_impl (unordered_pairs (glrs ~~ RCss))
   end
 
 
@@ -268,8 +263,8 @@
 (* if j < i, then turn around *)
 fun get_compat_thm thy cts eqvtsi eqvtsj i j ctxi ctxj =
   let
-    val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
-    val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
+    val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi
+    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)))
   in if j < i then
@@ -278,7 +273,7 @@
     in
       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 (rev eqvtsj) (* nominal *)
+      |> fold Thm.elim_implies eqvtsj (* 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" *)
@@ -289,7 +284,7 @@
     in
       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 (rev eqvtsi)  (* nominal *)
+      |> fold Thm.elim_implies eqvtsi  (* nominal *)
       |> fold Thm.elim_implies agsi
       |> fold Thm.elim_implies agsj
       |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
@@ -332,7 +327,7 @@
 fun mk_eqvt_lemma thy ih_eqvt clause =
   let
     val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
-
+     
     local open Conv in
       val ih_conv = arg1_conv o arg_conv o arg_conv
     end
@@ -420,7 +415,7 @@
         (llRI RS ih_intro_case)
         |> fold_rev (Thm.implies_intr o cprop_of) CCas
         |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
-
+ 
     val existence = fold (curry op COMP o prep_RC) RCs lGI
 
     val P = cterm_of thy (mk_eq (y, rhsC))
@@ -431,7 +426,7 @@
 
     fun elim_implies_eta A AB =
       Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
-
+ 
     val uniqueness = G_cases
       |> Thm.forall_elim (cterm_of thy lhs)
       |> Thm.forall_elim (cterm_of thy y)
@@ -963,7 +958,7 @@
       mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
 
     val compat =
-      mk_compat_proof_obligations domT ranT fvar f abstract_qglrs 
+      mk_compat_proof_obligations lthy domT ranT fvar f RCss abstract_qglrs 
       |> map (cert #> Thm.assume)
 
     val G_eqvt = mk_eqvt G |> cert |> Thm.assume