--- a/src/ZF/Tools/inductive_package.ML Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/Tools/inductive_package.ML Tue Jan 12 15:17:37 1999 +0100
@@ -141,7 +141,7 @@
val dummy =
if verbose then
- writeln ((if #1 (dest_Const Fp.oper) = "lfp" then "Inductive"
+ writeln ((if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then "Inductive"
else "Coinductive") ^ " definition " ^ big_rec_name)
else ();
@@ -528,7 +528,7 @@
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
val (thy2, induct, mutual_induct) =
- if #1 (dest_Const Fp.oper) = "lfp" then induction_rules raw_induct thy1
+ if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then induction_rules raw_induct thy1
else (thy1, raw_induct, TrueI)
and defs = big_rec_def :: part_rec_defs