--- a/src/CCL/Wfd.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/CCL/Wfd.thy Mon Jun 16 22:13:39 2008 +0200
@@ -55,7 +55,7 @@
ML {*
fun wfd_strengthen_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
+ res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
*}
lemma wf_anti_sym: "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P"
@@ -456,7 +456,7 @@
in
fun rcall_tac ctxt i =
- let fun tac ps rl i = RuleInsts.res_inst_tac ctxt ps rl i THEN atac i
+ let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i
in IHinst tac @{thms rcallTs} i end
THEN eresolve_tac @{thms rcall_lemmas} i
@@ -478,7 +478,7 @@
hyp_subst_tac)
fun clean_ccs_tac ctxt =
- let fun tac ps rl i = RuleInsts.eres_inst_tac ctxt ps rl i THEN atac i in
+ let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in
TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
hyp_subst_tac))