src/HOL/Tools/inductive_package.ML
changeset 24915 fc90277c0dd7
parent 24867 e5b55d7be9bb
child 24920 2a45e400fdad
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Oct 08 22:03:21 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 08 22:03:25 2007 +0200
     1.3 @@ -589,7 +589,7 @@
     1.4  fun mk_ind_def alt_name coind cs intr_ts monos
     1.5        params cnames_syn ctxt =
     1.6    let
     1.7 -    val fp_name = if coind then @{const_name FixedPoint.gfp} else @{const_name FixedPoint.lfp};
     1.8 +    val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
     1.9  
    1.10      val argTs = fold (fn c => fn Ts => Ts @
    1.11        (List.drop (binder_types (fastype_of c), length params) \\ Ts)) cs [];