diff -r 9294d7cec5e2 -r d9a0cf26a88c Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Sun Aug 08 10:12:38 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Wed Aug 11 16:21:24 2010 +0800
@@ -28,6 +28,8 @@
   val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> 
     term list -> thm -> thm list -> Proof.context -> thm list
   val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
+
+  val resolve_fun_rel: thm -> thm
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
@@ -604,7 +606,7 @@
 end
 
 
-(* helper lemmas for respectfulness for fv_raw / bn_raw *)
+(* respectfulness for fv_raw / bn_raw *)
 
 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
 let
@@ -622,7 +624,7 @@
     (K (asm_full_simp_tac ss)) ctxt
 end
 
-(* helper lemmas for respectfulness for size *)
+(* respectfulness for size *)
 
 fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
 let
@@ -641,5 +643,19 @@
   alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt
 end
 
+
+(* resolve with @{thm fun_relI} *)
+
+fun resolve_fun_rel thm =
+let 
+  val fun_rel = @{thm fun_relI}
+  val thm' = forall_intr_vars thm
+  val cinsts = Thm.match (cprem_of fun_rel 1, cprop_of thm')
+  val fun_rel' = Thm.instantiate cinsts fun_rel
+in
+  thm' COMP fun_rel'
+end 
+
+
 end (* structure *)