# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1281515030 -28800
# Node ID e2759a4dad4b8a1a965405efc4e7bcd975807539
# Parent  d9a0cf26a88c584f755f5c616a4c6aa9442279c0
updated to Isabelle 11 Aug

diff -r d9a0cf26a88c -r e2759a4dad4b Nominal/Rsp.thy
--- 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