src/CCL/Hered.thy
changeset 27239 f2f42f9fa09d
parent 27208 5fe899199f85
child 28262 aa7ca36d67fd
--- a/src/CCL/Hered.thy	Mon Jun 16 17:56:08 2008 +0200
+++ b/src/CCL/Hered.thy	Mon Jun 16 22:13:39 2008 +0200
@@ -97,8 +97,7 @@
   done
 
 ML {*
-  fun HTT_coinduct_tac ctxt s i =
-    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
+  fun HTT_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
 *}
 
 lemma HTT_coinduct3:
@@ -111,7 +110,7 @@
 val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
 
 fun HTT_coinduct3_tac ctxt s i =
-  RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
+  res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
 
 val HTTgenIs =
   map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})