src/LCF/LCF.thy

   adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
 
 
 ML {*
   fun induct_tac ctxt v i =
-    RuleInsts.res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
+    res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
     REPEAT (resolve_tac @{thms adm_lemmas} i)
 *}
 
 lemma least_FIX: "f(p) = p ==> FIX(f) << p"
   apply (tactic {* induct_tac @{context} "f" 1 *})

   apply (rule 3)
   done
 
 ML {*
 fun induct2_tac ctxt (f, g) i =
-  RuleInsts.res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
+  res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
   REPEAT(resolve_tac @{thms adm_lemmas} i)
 *}
 
 end