src/HOL/Tools/inductive_package.ML

 (** specification of (co)inductive predicates **)
 
 fun mk_ind_def alt_name coind cs intr_ts monos
       params cnames_syn ctxt =
   let
-    val fp_name = if coind then @{const_name FixedPoint.gfp} else @{const_name FixedPoint.lfp};
+    val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
 
     val argTs = fold (fn c => fn Ts => Ts @
       (List.drop (binder_types (fastype_of c), length params) \\ Ts)) cs [];
     val k = log 2 1 (length cs);
     val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;