--- a/Nominal/Rsp.thy	Wed Aug 11 16:21:24 2010 +0800
+++ b/Nominal/Rsp.thy	Wed Aug 11 16:23:50 2010 +0800
@@ -30,7 +30,7 @@
 fun get_rsp_goal thy trm =
 let
   val goalstate = Goal.init (cterm_of thy trm);
-  val tac = REPEAT o rtac @{thm fun_rel_id};
+  val tac = REPEAT o rtac @{thm fun_relI};
 in
   case (SINGLE (tac 1) goalstate) of
     NONE => error "rsp_goal failed"
@@ -48,7 +48,7 @@
   val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals)
   val user_thm = Goal.prove ctxt fixed' [] user_goal tac
   val user_thms = map repeat_mp (HOLogic.conj_elims user_thm)
-  fun tac _ = (REPEAT o rtac @{thm fun_rel_id} THEN' resolve_tac user_thms THEN_ALL_NEW atac) 1
+  fun tac _ = (REPEAT o rtac @{thm fun_relI} THEN' resolve_tac user_thms THEN_ALL_NEW atac) 1
   val rsp_thms = map (fn gl => Goal.prove ctxt [] [] gl tac) rsp_goals
 in
    ctxt