src/ZF/Tools/inductive_package.ML

   val big_rec_name = Sign.intern_const sign big_rec_base_name;
 
   
   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 ();
 
   (*Forbid the inductive definition structure from clashing with a theory
     name.  This restriction may become obsolete as ML is de-emphasized.*)

     end;  (*of induction_rules*)
 
   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
 
  in
    (thy2