src/CCL/Hered.thy

   apply (erule HTT_def [THEN def_coinduct])
   apply assumption
   done
 
 ML {*
-  fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] @{thm HTT_coinduct} i
+  fun HTT_coinduct_tac ctxt s i =
+    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
 *}
 
 lemma HTT_coinduct3:
   "[|  t : R;   R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT"
   apply (erule HTTgen_mono [THEN [3] HTT_def [THEN def_coinduct3]])

   done
 
 ML {*
 val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
 
-fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm HTT_coinduct3} i
+fun HTT_coinduct3_tac ctxt s i =
+  RuleInsts.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})
   ["true : HTTgen(R)",
    "false : HTTgen(R)",