--- a/src/HOL/Tools/inductive_package.ML Thu Oct 12 12:26:30 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML Thu Oct 12 13:01:19 2000 +0200
@@ -575,7 +575,7 @@
val induct = prove_goalw_cterm [] (cterm_of sign
(Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
[rtac (impI RS allI) 1,
- DETERM (etac (mono RS (fp_def RS def_induct)) 1),
+ DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
fold_goals_tac rec_sets_defs,
(*This CollectE and disjE separates out the introduction rules*)